Some Issues in Using Formal Methods for the Development of
Reactive Systems
Pablo Argón 1
Olivier Roux 1,2
- IRCyN (UMR 6597), 1 rue de la noe, 44321 NANTES (FRANCE). {argon|roux}@lan.ec-nantes.fr
- 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.