Formal Methods in System Design, 19, 81–110, 2001
c© 2001 Kluwer Academic Publishers. Manufactured in The Netherlands.
Formal Methods in Designing Embedded
Systems—the SACRES Experience
KLAUS WINKELMANN
∗
klaus.winkelmann@mchp.siemens.de
Siemens AG, ZT SE 4, Otto-Hahn-Ring 6, 81730 Mu¨nchen, Germany
Abstract. From automotive electronics to avionics, embedded systems are part of our everyday life, and de-
veloped 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.
Keywords: synchronous transition systems, DC+, state charts, SIGNAL, Statemate, Sildex, formal specification,
verification, model checking, symbolic timing diagrams, code generation, code validation, code distribution,
isochrony, endochrony
1. Introduction
1.1. Context and goals of the SACRES project
Embedded systems are an indispensable and critical ingredient of all industrial applications
as well as of our everyday lives. Some of these applications, such as automobiles and
aircraft, are safety-critical, i.e. a malfunction would cause severe material damage or even
endanger human health or lives. In less critical applications, e.g. in mobile phones or coffee
makers, failures are merely irritating, but the short development cycles demand a reliable
engineering method with predictable costs. The current state of the art is dominated by an
ad hoc mixture of methods and tools, and system validation is mostly done by extensive
testing at the implementation level.
∗
Many people contributed to the work reported here. See Section Acknowledgments for a complete list of
contributors to the project work.

82 WINKELMANN
In 1995, a consortium of academic as well as industrial R&D groups set out to integrate
their expertise in formal system design into a practical toolset that would give a new level
of quality to the design of embedded systems. SACRES aimed at increasing design quality,
avoiding unpredictability, decreasing design time and cost, and increasing maintainability,
changeability and reusability of complex embedded systems.
While the focus was on the development of safety-critical systems, the technology can
equally be used to develop any system where high-quality software is required.
As validation at the implementation level causes extreme and unpredictable effort in the
event of design errors being found, SACRES aims at early validation together with a high
degree of automation.
1.2. The proposed design flow
A successful use of formal methods requires not just new tools, but a clear view of how, why
and where to use such tools in the design flow. The design flow as proposed in SACRES is
depicted in figure 1, and is characterised by the following guidelines:
• At the level of requirement capture, use formal specification of safety-critical properties
for maximum rigour.
• Rather than defining a new language for specifying systems, make use of existing design
tools and languages. This is a very important choice, as it greatly increases the acceptance
of the methodology: for a user, switching to a completely new front-end, tempting as
Figure 1. SACRES support in the design flow.