In: Proc. 26th EUROMICRO Conference, 5-7 September 2000, Maastricht, The Netherlands, Vol. 1, pages 106-113. 2000.
Abstract: The complexity of embedded systems is increasing rapidly. In consequence, new verification techniques that overcome the limitations of traditional methods and are suitable for hardware/software systems are needed. This paper introduces a computational model for embedded systems based on Petri nets, called PRES. An approach to coverification of both the hardware and software parts of an embedded system represented by PRES is presented. Symbolic model checking is used to prove the correctness of such systems, specifying properties in CTL and verifying whether they are satisfied. This coverification method permits to reason formally about the design properties as well as timing requirements. A medical monitoring system illustrates the feasibility of the approach on practical applications.
Keywords: PRES, Petri nets, embedded systems, formal coverification, symbolic model checking.