Paper Info
Title
Automated validation of software models
Abstract
The paper describes the application of an automated verification tool to a software model developed at Ford Motor Company. Ford already has in place an advanced model-based software development framework that employs the Matlab(R), Simulink(R), and Stateflow(R) modeling tools. During this project, we applied the invariant checker Salsa to a Simulink(R)/Stateflow(R) 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.
Year
DOI
Venue
2001
10.1109/ASE.2001.989794
Automated Software Engineering, 2001.
Keywords
Field
DocType
automotive software,invariant checker,advanced model-based softwaredevelopment framework,redundant code,modeling tools,matlab,salsa,automotive software tocheck,cost-effective application,automated software model validation,software model,andredundant code,stateflow,automobiles,advanced model-based software development framework,ford motor company,anomaly detection,dead code,automatic programming,nondeterminism,missing case,invariant checker salsa,software models,missing cases,simulink,automated validation,automatedverification tool,program verification,formal specification,formal verification,automated verification tool
Static program analysis,Programming language,Software engineering,Computer science,Stateflow,Software construction,Software verification and validation,Software measurement,Software sizing,Software framework,Software verification
Conference
ISSN
ISBN
Citations 
1938-4300
0-7695-1426-X
23
PageRank 
References 
Authors
1.80
7
4
Name
Order
Citations
PageRank
Steve Sims1231.80
Rance Cleaveland22266254.39
Ken Butts316116.23
Scott Ranville4231.80