@conference {10.1007/3-540-60406-5_7, title = {Using a symbolic model checker for verify safety properties in SA/RT models}, booktitle = {Software Engineering {\textendash}- ESEC {\textquoteright}95}, year = {1995}, pages = {59{\textendash}75}, publisher = {Springer Berlin Heidelberg}, organization = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, 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).}, isbn = {978-3-540-45552-3}, author = {Tuya, Javier and S{\'a}nchez, Luciano and Corrales, Jose A.}, editor = {Sch{\"a}fer, Wilhelm and Botella, Pere} }