Subir material

Suba sus trabajos a SEDICI, para mejorar notoriamente su visibilidad e impacto

 

Mostrar el registro sencillo del ítem

dc.date.accessioned 2022-05-03T19:10:28Z
dc.date.available 2022-05-03T19:10:28Z
dc.date.issued 1998-06-26
dc.identifier.uri http://sedici.unlp.edu.ar/handle/10915/135553
dc.description.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. en
dc.format.extent 52-75 es
dc.language en es
dc.subject Compiler design es
dc.subject Coq theorem prover es
dc.subject Electre reactive language es
dc.subject program proof es
dc.subject program extraction es
dc.subject Model checking es
dc.subject Spin model checker es
dc.title Some Issues in Using Formal Methods for the Development of Reactive Systems en
dc.type Articulo es
sedici.identifier.uri https://publicaciones.sadio.org.ar/index.php/EJS/article/view/135 es
sedici.identifier.issn 1514-6774 es
sedici.creator.person Argón, Pablo es
sedici.creator.person Roux, Olivier es
sedici.subject.materias Ciencias Informáticas es
sedici.description.fulltext true es
mods.originInfo.place Sociedad Argentina de Informática e Investigación Operativa es
sedici.subtype Articulo es
sedici.rights.license Creative Commons Attribution 4.0 International (CC BY 4.0)
sedici.rights.uri http://creativecommons.org/licenses/by/4.0/
sedici.relation.journalTitle Electronic Journal of SADIO es
sedici.relation.journalVolumeAndIssue vol. 1 es


Descargar archivos

Thumbnail
Documento
Descargar archivo (359.8Kb) - PDF
Icon
Enlace externo

Este ítem aparece en la(s) siguiente(s) colección(ones)

Creative Commons Attribution 4.0 International (CC BY 4.0) Excepto donde se diga explícitamente, este item se publica bajo la siguiente licencia Creative Commons Attribution 4.0 International (CC BY 4.0)