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.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||