Formal methods in designing embedded systems-the SACRES experience
From automotive electronics to avionics, embedded systems are part of our everyday life, and developed societies are increasingly dependent on their reliability in operation. At the same time, current design practice is inadequate in coping with the challenge of constructing dependable embedded systems. SACRES is an experimental design environment aimed at the seamless development of embedded systems. It incorporates state-of-the-art industrial design tools and provides formal specification, model checking technology and validated code generation. These concepts have been integrated on the basis of the synchronous approach to reactive systems. As a result, synchronous compilation techniques have been enhanced, in particular as regards techniques for distributed code generation. Formal verification technology was advanced to increase efficiency, handle composed systems and cover some real-time aspects. The new approach of translation validation was developed and proven to work. Real bugs have been found even in well-tested models. It was demonstrated that a formal design including verification is often more efficient than testing. As a consequence, all user partners are committed to further introducing formal design and verification technology. This paper summarises the essential achievements of the project. It explains the results in terms of the basic ideas, the available tools and methodology, as well as the experience gained.
formal specification model checking code generation verification synchronous transition systems dc state charts signal statemate sildex symbolic timing diagrams code validation code distribution isochrony endochrony