16th IEEE International Conference on Automated Software Engineering (ASE'01) Automated Validation of Software Models San Diego, California November 26-November 29 ISBN: 0-7695-1426-X
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.
Citation:
Steve Sims, Rance Cleaveland, Ken Butts, Scott Ranville, "Automated Validation of Software Models," ase, pp.91, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||