Combination of Formal and Informal Approaches
to Validate Embedded Software

Francesca Saglietti
Institute for Safety Technology (ISTec) GmbH
Forschungsgelände 85748 Garching Germany






Thanks to the flexibility provided by software-based components, the diffusion of embedded controllers in safety-relevant applications is continuously expanding; for similar reasons, also the complexity of safety-critical functionalities is increasing. The considerable progress achieved during the last decade in the area of formal methods has reduced one main source of faults, namely those caused by erroneous implementation; the growing responsibility of software controllers for complex tasks tends, however, to shift the major source of problems from the actual software development phases up towards the earlier phases of requirements analysis.

The talk will analyse formal and informal techniques applied to verify and validate software-based embedded systems, especially in case of safety-relevant applications. It will focus on the strength of each class and will illustrate their limits in the light of some recent real-world accidents, mostly related to incomplete or erroneous requirements. The main lesson to be learnt from these failures is the need for combining formal and informal techniques in order to support the rigorous representation, analysis and validation of requirements in the early, not fully formalizable design phases. Two different examples are chosen to illustrate this approach.

The first one focuses on hybrid modelling languages (like Time Petri Nets), allowing the integration of logical discreteness and physical continuity. A systematic analysis of safety-related system properties supports the early identification of weak design assumptions.

The second approach aims at supporting design for safety by applying formal decisions to optimize checkpointing when implementing fault-tolerant software. During code execution a formal mechanism is responsible for interrupting the ongoing operation and check intermediate values, or for proceeding and postponing the check. Like for other areas of safety engineering, the use of binary decision diagrams is recommended.