Using a symbolic model checker for verify safety properties in SA/RT models

Comunicación en congreso 1995

Javier Tuya, Luciano Sánchez, Jose Corrales

Páginas 59-75

Google Scholar Todas las publicaciones

Cómo citar esta publicación

Tuya, J., Sánchez, L., & Corrales, J. A. (1995). Using a symbolic model checker for verify safety properties in SA/RT models (W. Schäfer & P. Botella, Eds.). Berlin, Heidelberg: Springer Berlin Heidelberg.
BibTeX

Resumen

In this paper, structured methods are integrated with formal verification methods based on temporal logic. The goal is to use an operational method (SA/RT) for the system behavioural specification, and to complement this with safety properties expressed in a declarative style using temporal logic (CTL). These properties are checked against the operational specification using a model checker (SMV).

Detalles

Editores
Wilhelm Schäfer, Pere Botella
Editorial
Springer Berlin Heidelberg
Lugar del congreso
Berlin, Heidelberg
ISBN
978-3-540-45552-3