A New Formal Verification Approach for Hardware-dependent Embedded System Software
スポンサーリンク
概要
- 論文の詳細を見る
This paper describes a method to generate a computational model for formal verification of hardware-dependent software in embedded systems. The computational model of the combined HW/SW system is a program netlist (PN) consisting of instruction cells connected in a directed acyclic graph that compactly represents all execution paths of the software. The model can be easily integrated into SAT-based verification environments such as those based on Bounded Model Checking (BMC). The proposed construction of the model allows for an efficient reasoning of the SAT solver over entire execution paths. Program netlists are compositional. The paper presents how they can be combined to model interrupt-driven systems. We demonstrate the efficiency of our approach by presenting experimental results from the formal verification of an industrial LIN (Local Interconnect Network) bus node, implemented as a software driver on a 32-bit RISC machine.
著者
-
Nguyen Minh
Hanoi University of Science and Technology
-
Schmidt Bernard
University of Kaiserslautern
-
Stoffel Dominik
University of Kaiserslautern
-
Kunz Wolfgang
University of Kaiserslautern
-
Villarraga Carlos
University of Kaiserslautern
-
Fehmel Thomas
University of Kaiserslautern