@conference {12823,
	title = {Automated Validation of Software Models},
	booktitle = {Automated Software Engineering, International Conference on},
	year = {2001},
	month = {2001///},
	pages = {91 - 91},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Los Alamitos, CA, USA},
	abstract = {This paper describes the application of an automated verification tool to a software model developed at Ford. Ford already has in place an advanced model-based software development framework that employs the Matlab?, Simulink?, and Stateflow? modeling tools. During this project we applied the invariant checker Salsa to a Simulink?/ Stateflow? model of automotive software to check for nondeterminism, missing cases, dead code, and redundant code. During the analysis, a number of anomalies were detected that had not been found during manual review. We argue that the detection and correction of these problems demonstrates a cost-effective application of formal verification that elevates our level of confidence in the model.},
	isbn = {0-7695-1426-X},
	doi = {http://doi.ieeecomputersociety.org/10.1109/ASE.2001.989794},
	author = {Sims,Steve and Cleaveland, Rance and Butts,Ken and Ranville,Scott}
}
