Integrating Formal Methods into the Development Cycle of a Safety-critical Embedded Software System

This paper describes a technology transfer project where formal specification and verification techniques have been applied in the development of a safety-critical embedded software system. IRST was directly involved in the development of the system, jointly working with the design engineers of a leading company in the design of embedded systems. The project was subject to two major requirements. First, a tight integration of the informal methodologies into the existing development cycle was to be achieved in order to enhance the quality of the design. Second, it was necessary to limit the impact of a new , potentially costly methodology. During the project, a structured specification methodology was designed, tailored to the structure of the system under analysis. This methodology combines the use of the commercial tool OBJECTGEODE with a custom support tool, developed during the project, for the automatic generation of executable models, starting from the formal specification of sub-component