Some Issues in Using Formal Methods for the Development of Reactive Systems

Pablo Argón 1 Olivier Roux 1,2

1. IRCyN (UMR 6597), 1 rue de la noe, 44321 NANTES (FRANCE). {argon|roux}@lan.ec-nantes.fr
2. Institut Universitarie de France

Abstract:

For the development of safety-critical reactive systems, proving correctness is unavoidable. Here we describe some research issues on using and combining formal methods. Using the Electre reactive language we illustrate a technique to the design of a sound compiler with the Coq theorem prover. Based on the same source language semantic model, we present the outlines of a method to verify correctness claims with the SPIN model checker.

Keywords: Compiler design, Coq theorem prover, Electre reactive language, program proof, program extraction, model checking, Spin model checker.