@inproceedings{1,
  author = {Javier Tuya and Luciano Sánchez and Jose Corrales},
  editor = {Wilhelm Schäfer and Pere Botella},
  title = {Using a symbolic model checker for verify safety properties in SA/RT models},
  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).},
  year = {1995},
  pages = {59-75},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  isbn = {978-3-540-45552-3},
}