Automated Validation of Software Models

Steve Sims, Rance Cleaveland, Ken Butts, Scott Ranville

DOI 10.1109/ase.2001.989794 dblp

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.

BibTeX

@inproceedings{Sims-al:ASE01,
  author    = {Steve Sims and
               Rance Cleaveland and
               Ken Butts and
               Scott Ranville},
  title     = {Automated Validation of Software Models},
  booktitle = {ASE},
  pages     = {91-},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Automated Validation of Software Models

Abstract

Related papers