Verification of Embedded Systems using a Petri Net based Representation
13th International Symposium on System Synthesis (ISSS 2000), Madrid, Spain, Sept. 2022, 2000, pp. 149155.
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.pdf  Adobe Acrobat portable document 
ISSS00.ps.gz  postscript 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. 2022, 2000, pp. 149155. 
