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

Verification of Heterogeneous Electronic Systems using Model Checking

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

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

ABSTRACT
The ever increasing complexity of heterogeneous electronic systems consisting of hardware and software components poses a challenge in verifying their correctness. The complexity of this kind of systems is such, that traditional validation methods, like simulation and testing, are not enough to verify their correctness. In consequence, new verification methods that over-come the limitations of traditional techniques and, at the same time, are suitable for heteroge-neous hardware/software systems are needed. In this report we formally define the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. We introduce an approach to formal verification of heterogeneous electronic systems: we make use of model checking to prove the correctness of such systems by determining the truth of CTL and TCTL formulas that specify required properties with respect to a PRES+ model. Thus verification with timing properties is possible. An ATM server illustrates the feasibility of this approach on practical applications. 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:
SAVE00.pdfAdobe Acrobat portable document
SAVE00.ps.gzpostscript document, compressed (with gzip)


[AEP00] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Verification of Heterogeneous Electronic Systems using Model Checking", SAVE Project Report, Dept. of Computer and Information Science, Linköping University, July 2000.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)