@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}
}
