Automated Validation of Software Models

TitleAutomated Validation of Software Models
Publication TypeConference Papers
Year of Publication2001
AuthorsSims S, Cleaveland R, Butts K, Ranville S
Conference NameAutomated Software Engineering, International Conference on
Date Published2001///
PublisherIEEE Computer Society
Conference LocationLos Alamitos, CA, USA
ISBN Number0-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.