In: Proc. 13th Int. Symp. on System Synthesis (SSS'2000), 20-22 September 2000, Madrid, Spain, pages 149-155. 2000.
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. This paper formally defines the semantics of PRES+, a Petri net based computational model aimed to represent embedded systems. An approach to formal verification of such systems is introduced by using 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 the proposed approach on practical applications.
Keywords: PRES+, Petri nets, embedded systems, system verification.
Back to the Petri Nets Bibliography