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

Modeling and Formal Verification of Embedded Systems based on a Petri Net Representation

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

Journal of Systems Architecture (JSA), Special Issue on System and Circuit Synthesis and Verification, vol. 49, no. 12-15, December 2003, pp. 571-598.

ABSTRACT
In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.


Related files:
JSA03.pdfAdobe Acrobat portable document


[AEP03] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Modeling and Formal Verification of Embedded Systems based on a Petri Net Representation", Journal of Systems Architecture (JSA), Special Issue on System and Circuit Synthesis and Verification, vol. 49, no. 12-15, December 2003, pp. 571-598.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)