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

Autores/as

  • Pablo Argón Institut de Recherche en Cybern'etique de Nantes, Francia
  • Olivier Roux Institut de Recherche en Cybern'etique de Nantes, Francia

Palabras clave:

compiler design, Coq theorem prover, electre reactive language, program proof, program extraction, model checking, spin model checker

Resumen

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.

Descargas

Publicado

1998-06-01

Número

Vol. 1 (1998): Electronic Journal of SADIO (EJS) Vol. 1 (1998)

Sección

Papers

Licencia

Derechos de autor 1998 Pablo Argón, Olivier Roux

Creative Commons License

Esta obra está bajo una licencia internacional Creative Commons Atribución-NoComercial-CompartirIgual 4.0.

Aquellos autores/as que tengan publicaciones con esta revista, aceptan los términos siguientes:

  1. Los autores/as conservarán sus derechos de autor y garantizarán a la revista el derecho de primera publicación de su obra, el cuál estará simultáneamente sujeto a la Creative Commons Atribución-NoComercial-CompartirIgual 4.0 Internacional (CC BY-NC-SA 4.0) que permite a terceros compartir la obra siempre que se indique su autor y su primera publicación esta revista, no hagan uso comercial de ella y las obras derivadas de hagan bajo la misma licencia.
  2. Los autores/as podrán adoptar otros acuerdos de licencia no exclusiva de distribución de la versión de la obra publicada (p. ej.: depositarla en un archivo telemático institucional o publicarla en un volumen monográfico) siempre que se indique la publicación inicial en esta revista.
  3. Se permite y recomienda a los autores/as difundir su obra a través de Internet (p. ej.: en archivos telemáticos institucionales o en su página web) antes y durante el proceso de envío, lo cual puede producir intercambios interesantes y aumentar las citas de la obra publicada. (Véase El efecto del acceso abierto).

Cómo citar

Argón, P., & Roux, O. (1998). Some Issues in Using Formal Methods for the Development of Reactive Systems. SADIO Electronic Journal of Informatics and Operations Research, 1, 52-75. https://revistas.unlp.edu.ar/ejs/article/view/17504