HW/SW co-verification of embedded systems using bounded model checking
HW/SW co-verification of embedded systems using bounded model checking
复制标题
使用有界模型检查对嵌入式系统进行硬件/软件协同验证
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Daniel Große;U. Kühne;R. Drechsler
今天，嵌入式系统的底层硬件经常被成功验证。在这种情况下，形式化验证技术允许证明功能的正确性。但在嵌入式系统设计中，软件构件的集成变得越来越重要。在本文中，我们提出了一种集成的硬件和软件形式化验证方法。该方法在RISC CPU上进行了演示。验证基于有界模型检测。除了底层硬件、硬件/软件接口和使用该接口的程序的正确性证明外，还可以对其进行正式验证。
Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes more and more important. In this paper we present an integrated approach for formal verification of hardware and software. The approach is demonstrated on a RISC CPU. The verification is based on bounded model checking. Besides correctness proofs of the underlying hardware the hardware/software interface and programs using this interface can be formally verified.