loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Steve Sims, Reactive Systems, Inc.
Rance Cleaveland, Reactive Systems, Inc.
Ken Butts, Ford Motor Company
Scott Ranville, New Eagle Software
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.