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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Argón, Pablo, Roux, Olivier
Formato: Articulo
Lenguaje:Inglés
Publicado: 1998
Materias:
Ciencias Informáticas
Compiler design
Coq theorem prover
Electre reactive language
program proof
program extraction
Model checking
Spin model checker
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:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-135553
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Compiler design
Coq theorem prover
Electre reactive language
program proof
program extraction
Model checking
Spin model checker
spellingShingle Ciencias Informáticas
Compiler design
Coq theorem prover
Electre reactive language
program proof
program extraction
Model checking
Spin model checker
Argón, Pablo
Roux, Olivier
Some Issues in Using Formal Methods for the Development of Reactive Systems
topic_facet Ciencias Informáticas
Compiler design
Coq theorem prover
Electre reactive language
program proof
program extraction
Model checking
Spin model checker
description 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.
format Articulo
Articulo
author Argón, Pablo
Roux, Olivier
author_facet Argón, Pablo
Roux, Olivier
author_sort Argón, Pablo
title Some Issues in Using Formal Methods for the Development of Reactive Systems
title_short Some Issues in Using Formal Methods for the Development of Reactive Systems
title_full Some Issues in Using Formal Methods for the Development of Reactive Systems
title_fullStr Some Issues in Using Formal Methods for the Development of Reactive Systems
title_full_unstemmed Some Issues in Using Formal Methods for the Development of Reactive Systems
title_sort some issues in using formal methods for the development of reactive systems
publishDate 1998
url http://sedici.unlp.edu.ar/handle/10915/135553
https://publicaciones.sadio.org.ar/index.php/EJS/article/view/135
work_keys_str_mv AT argonpablo someissuesinusingformalmethodsforthedevelopmentofreactivesystems
AT rouxolivier someissuesinusingformalmethodsforthedevelopmentofreactivesystems
bdutipo_str Repositorios
_version_ 1764820455464632321

Ejemplares similares