Verification of Embedded Systems using a Petri Net based Representation

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 toformal verification of such systems: we make use of model checking to prove the correctness of embedded systems by determining the truth of CTL and TCTLformulas that specify requiredproperties with respect to a PRES+ model. An ATM server illustrates thefeasibility of our approach on practical applications.

• Type: Conference
• Year: 2000
• Where: ISSS
• Authors: Luis Alejandro Cortés, Petru Eles, Zebo Peng
• Keywords: Approach Toformal Verification, Embedded Systems, Hardware, Hardware/ Software Systems, ISSS 2000