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

Conference Paper 1995

Javier Tuya, Luciano Sánchez, Jose Corrales

Pages 59-75

Google Scholar All publications

Cite this publication

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

Abstract

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

Details

Editors
Wilhelm Schäfer, Pere Botella
Publisher
Springer Berlin Heidelberg
Conference Location
Berlin, Heidelberg
ISBN Number
978-3-540-45552-3