Linköping University: Students Alumni Trade and Industry/Society Internal Search
ICECCS00

Definitions of Equivalence for Transformational Synthesis of Embedded Systems

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

6th International Conference on Engineering of Complex Computer Systems (ICECCS 2000), Tokyo, Japan, Sept. 11-15, 2000, pp. 134-142.

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. In this paper we present 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 our notation, hold information and transitionsÑwhen firedÑperform transformation of data. Based on this model we define several notions of equivalence (reachable, behavioral, time, and total), which provide the framework for transformational synthesis of embedded systems. 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.


Related files:
ICECCS00.pdfAdobe Acrobat portable document
ICECCS00.ps.gzpostscript document, compressed (with gzip)


[AEP00] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Definitions of Equivalence for Transformational Synthesis of Embedded Systems", 6th International Conference on Engineering of Complex Computer Systems (ICECCS 2000), Tokyo, Japan, Sept. 11-15, 2000, pp. 134-142.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)