Formal methods for the verification of embedded systems

Embedded systems are subject to many constraints, and some interact closely with hazardous processes, or are involved in decision-making processes that impact on human lives. The development of such systems must offer guarantees of correct operation and recovery in the event of failure of an internal part or an unforeseen environment.

Formal verification methods can be implemented to increase system confidence. Three main classes can be distinguished:

• theorem-proving ;

• model-checking and its many variants and extensions;

  specification refinement.

The positioning of these approaches in the design flow of embedded systems is presented.

For each approach, we simply present the basic principle, the main field of application, the tools available and academic and industrial achievements. This article does not use advanced mathematical formalism, so as to be accessible to as many people as possible. The bibliographical references provide more detailed information on the formal aspects of each approach, as well as on the tools available and (where applicable) their use in an industrial context.