Title | Using a symbolic model checker for verify safety properties in SA/RT models |
Publication Type | Conference Paper |
Year of Publication | 1995 |
Authors | Tuya, Javier, Sánchez Luciano, and Corrales Jose A. |
Editor | Schäfer, Wilhelm, and Botella Pere |
Conference Name | Software Engineering –- ESEC '95 |
Pagination | 59–75 |
Publisher | Springer Berlin Heidelberg |
Conference Location | Berlin, Heidelberg |
ISBN Number | 978-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). |