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

TitleUsing a symbolic model checker for verify safety properties in SA/RT models
Publication TypeConference Paper
Year of Publication1995
AuthorsTuya, Javier, Sánchez Luciano, and Corrales Jose A.
EditorSchäfer, Wilhelm, and Botella Pere
Conference NameSoftware Engineering –- ESEC '95
Pagination59–75
PublisherSpringer Berlin Heidelberg
Conference LocationBerlin, Heidelberg
ISBN Number978-3-540-45552-3
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).