View article

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 (Computation Tree Logic) and TCTL (Timed CTL) formulas that specify required properties with respect to a PRES+ model. An ATM server illustrates the feasibility of our approach on practical applications.