Verification Methodology for Heterogeneous Hardware/Software Systems
SAVE Project Report, Dept. of Computer and Information Science, Linköping University, January 2000.
Modern electronic systems are constituted by heterogeneous elements, e.g. hardware/software, and are typically embedded. The complexity of this kind of systems is such, that traditional validation techniques, like simulation and testing, are not enough to verify the correctness of these systems. In consequence, new formal verification techniques that overcome the limitations of traditional validation methods and are suitable for hardware/software systems are needed. Formal methods require the system to be represented by a formal computational model with clear semantics. We present a Petri net based representation, called PRES, which is able to capture information relevant to embedded systems. This report also explores an approach to formal verification of embedded systems in which the underlying representation is PRES. We use symbolic model checking to prove the correctness of such systems, specifying properties in CTL and verifying whether they hold under all possible situations. This coverification method permits to reason formally about design properties as well as timing requirements. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous electronic systems.
[AEP00] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Verification Methodology for Heterogeneous Hardware/Software Systems", SAVE Project Report, Dept. of Computer and Information Science, Linköping University, January 2000.