In: Proc. 6th IEEE Int. Conf. on Engineering of Complex Computer Systems, 11-14 September 2000, Tokyo, Japan, pages 134-142. 2000.
Abstract: Design of embedded systems is a complex task that requires design cycles founded upon formal notation, so that the synthesis from specification to implementation can be carried out systematically. This paper presents a computational model for embedded systems based on Petri nets called PRES+. It includes an explicit notion of time and allows a concise formulation of models. Tokens, in the proposed notation, hold information and transitions, when fired, perform transformation of data. Several notions of equivalence (reachable, behavioral, time and total), which provide the framework for transformational synthesis of embedded systems, are defined using this model. Different representations of an Ethernet network coprocessor are studied in order to illustrate the applicability of PRES+ and the definitions of equivalence on practical systems.
Keywords: PRES+, Petri nets, embedded systems, transformational synthesis.