Some Issues in Using Formal Methods for the Development of Reactive Systems
Keywords:
compiler design, Coq theorem prover, electre reactive language, program proof, program extraction, model checking, spin model checkerAbstract
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.
Downloads
Published
Issue
Section
License
Copyright (c) 1998 Pablo Argón, Olivier Roux
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Those authors who have publications with this journal, agree with the following terms:
a. Authors will retain its copyright and will ensure the rights of first publication of its work to the journal, which will be at the same time subject to the Creative Commons Atribución-NoComercial-CompartirIgual 4.0 Internacional (CC BY-NC-SA 4.0) allowing third parties to share the work as long as the author and the first publication on this journal is indicated.
b. Authors may elect other non-exclusive license agreements of the distribution of the published work (for example: locate it on an institutional telematics file or publish it on an monographic volume) as long as the first publication on this journal is indicated,
c. Authors are allowed and suggested to disseminate its work through the internet (for example: in institutional telematics files or in their website) before and during the submission process, which could produce interesting exchanges and increase the references of the published work. (see The effect of open Access)
