Some Issues in Using Formal Methods for the Development of Reactive Systems
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...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Articulo |
| Lenguaje: | Inglés |
| Publicado: |
1998
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/135553 https://publicaciones.sadio.org.ar/index.php/EJS/article/view/135 |
| Aporte de: |
| Sumario: | 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. |
|---|