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 tech-niques and, at the same time, are suitable for hardware/ software systems are needed. In this work we formally de-fine the semantics of PRES+, a Petri net based computa-tional model aimed to represent embedded systems. We introduce an approach to formal verification of such sys-tems: we make use of model checking to prove the correct-ness of embedded systems by determining the truth of CTL and TCTL formulas that specify required properties with re-spect to a PRES+ model. An ATM server illustrates the fea-sibility of our approach on practical applications. 1