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

Verification of Embedded Systems using a Petri Net based Representation

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

13th International Symposium on System Synthesis (ISSS 2000), Madrid, Spain, Sept. 20-22, 2000, pp. 149-155.

ABSTRACT
The ever increasing complexity of embedded systems consisting of hardware and software components poses a challenge in verifying their correctness. New verification methods that overcome the limitations of traditional techniques and, at the same time, are suitable for hardware/software systems are needed. In this work 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 such systems: we make use of model checking to prove the correctness of embedded systems by determining the truth of CTL and TCTL formulas that specify required properties with respect to a PRES+ model. An ATM server illustrates the feasibility of our approach on practical applications.


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


[AEP00] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Verification of Embedded Systems using a Petri Net based Representation", 13th International Symposium on System Synthesis (ISSS 2000), Madrid, Spain, Sept. 20-22, 2000, pp. 149-155.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)