In: Proceedings of Applications and Theory of Petri Nets 2004: 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, pages 35-36. Volume 3099 of Lecture Notes in Computer Science / Cortadella, Reisig (Eds.) --- Springer-Verlag, September 2004.
Abstract: Embedded software is increasingly deployed in safety-critical applications, from medical implants to drive-by-wire technology. This calls for a rigorous design and verification methodology. The main difference between embedded and traditional software is that in the embedded case non-functional aspects, such as reactivity with respect to physical processes, resource usage, and timing, are integral to the correct behavior of the software. Yet traditional software description mechanisms -- including specification, modeling, and programming languages -- rarely address these non-functional aspects; indeed, the systematic abstraction of real time and other physical constraints in models of sequential and concurrent computation, from Turing machines to software threads, has been one of the great success stories in computer science. For the principled design of embedded software, instead, we have to recombine computation and physicality.