Linköping University: Students Alumni Trade and Industry/Society Internal Search
SAVE99b

Verification Methodology for Heterogeneous Hardware/Software Systems

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

SAVE Project Report, Dept. of Computer and Information Science, Linköping University, January 2000.

ABSTRACT
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.


Related files:
SAVE99b.pdfAdobe Acrobat portable document
SAVE99b.ps.gzpostscript document, compressed (with gzip)


[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.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)