Improving System-Level Verification of SystemC Models with SPIN
Improving System-Level Verification of SystemC Models with SPIN
复制标题
使用 SPIN 改进 SystemC 模型的系统级验证
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
P. Puschner
中科院分区：
文献类型：
--
作者：
Martin Elshuber;Susanne Kandl;P. Puschner
SystemC是开发，建模和模拟嵌入式系统的事实行业标准。随着嵌入式系统越来越融入人类生活的许多方面（例如，运输，监视系统，...），嵌入式系统的故障可能会对个人或群体造成危险的危害。确保此类系统的安全至关重要。在本文中，我们提出了一种用自旋验证Systemc模型的新方法。重点关注系统级验证，我们从原始模型重复使用并可执行代码，并将其嵌入由旋转生成的验证者中。与大多数其他需要完整模型转换的方法相反，在我们的方法中，转换仅集中在模型的相关部分，同时使功能块未转换。我们的技术旨在减少由自旋验证器管理的状态向量大小，通过避免不必要的模型转换步骤来改善状态勘探性能，并专注于验证从多个功能单元组成中出现的验证属性。
SystemC is a de-facto industry standard for developing, modelling, and simulating embedded systems. As embedded systems become more and more integrated into many aspects of human lives (e.g., transportation, surveillance systems, ...), failures of embedded systems might cause dangerous hazards to individuals or groups. Guaranteeing safety of such systems makes formal verification crucial. In this paper we present a novel approach for verifying SystemC models with SPIN. Focusing on system-level verification we reuse compiled and executable code from the original model and embed it into the verifier generated by SPIN. In contrast to most other approaches, which require a complete model transformation, in our approach the transformation focuses only on the relevant parts of the model while leaving functional blocks untransformed. Our technique aims at reducing the state vector size managed by the verifier of SPIN, at improving state exploration performance by avoiding unnecessary model transformation steps, and at concentrating on verifying properties that emerge from the composition of multiple functional units.