Article

Automated Validation of Software Models

Authors:

Steve Sims,

Rance Cleaveland,

Ken Butts,

Scott RanvilleAuthors Info & Claims

ASE '01: Proceedings of the 16th IEEE international conference on Automated software engineering

Page 91

Published: 26 November 2001 Publication History

Publisher Site

Abstract

This paper describes the application of an automatedverification tool to a software model developed at Ford.Ford already has in place an advanced model-based softwaredevelopment framework that employs the Matlab®,Simulink®, and Stateflow® modeling tools. Duringthis project we applied the invariant checker Salsa to aSimulink®/ Stateflow® model of automotive software tocheck for nondeterminism, missing cases, dead code, andredundant code. During the analysis, a number of anomalieswere detected that had not been found during manualreview. We argue that the detection and correction of theseproblems demonstrates a cost-effective application of formalverification that elevates our level of confidence in themodel.

References

[1]

K. Butts, J. Cook, C. Davey, J. Friedman, P. Menter, S. Raman, N. Sivashankar, P. Smith, and S. Toeppe. Automotive powertrain controller development using CACSD. In Tariq Samad, editor, Perspectives in Control Engineering: Technologies, Applications, and New Directions. IEEE Press, 2001.

Google Scholar

[2]

R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.

Digital Library

Google Scholar

[3]

R. Bharadwaj and S. Sims. Salsa: Combining constraint solvers with BDDs for automatic invariant checking. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '00), Berlin, March 2000. Springer-Verlag.

Digital Library

Google Scholar

[4]

R. Cleaveland and S. Sims. The NCSU Concurrency Workbench. In R. Alur and T. Henzinger, editors, Computer Aided Verification (CAV '96), Lecture Notes in Computer Science, pages 394-397, New Brunswick, New Jersey, July 1996. Springer-Verlag.

Digital Library

Google Scholar

[5]

C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231-261, July 1996.

Digital Library

Google Scholar

[6]

M. Heimdahl and N. Leveson. Completeness and consistency in hierarchical state-based requirements, 1996.

Digital Library

Google Scholar

[7]

G. J. Holzmann. The model checker SPIN. IEEE Trans. on Softw. Eng., 23(5):279-295, May 1997.

Digital Library

Google Scholar

[8]

David Harel and Michal Politi. Modeling Reactive Systems With Statecharts. McGraw-Hill, 1998.

Digital Library

Google Scholar

[9]

Home page of The Mathworks, Inc. http://www.mathworks.com/.

Google Scholar

[10]

K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[11]

P. Smith, S. Patel, W. Sun, R. Ramanan, H. Donald, S. Toeppe, S. Ranville, D. Bostic, and K. Butts. CACSD in production development : An engine control case study. In Proceedings of the Global Powertrain Congress, Detroit, MI, June 2000.

Google Scholar

[12]

S. Toeppe and S. Ranville. An automated inspection tool for a graphical specification and progranming language. In Proceedings of the 12th International Software Quality Week Conference, San Jose, CA, May 1999.

Google Scholar

Cited By

View all

Chowdhury SShrestha SJohnson TCsallner CRothermel GBae D(2020)SLEMIProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380381(335-346)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380381
Chowdhury SMohian SMehra SGawsane SJohnson TCsallner CChaudron MCrnkovic IChechik MHarman M(2018)Automatically finding bugs in a commercial cyber-physical system development tool chain with SLforgeProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180231(981-992)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180231
Elberzhager FRosbach ABauer TCarrozza GPietrantuono RManetti V(2013)Analysis and testing of matlab simulink models: a systematic mapping studyProceedings of the 2013 International Workshop on Joining AcadeMiA and Industry Contributions to testing Automation10.1145/2489280.2489285(29-34)Online publication date: 15-Jul-2013
https://dl.acm.org/doi/10.1145/2489280.2489285
Show More Cited By

Recommendations

Resolving Linkage Anomalies in Extracted Software System Models
IWPC '04: Proceedings of the 12th IEEE International Workshop on Program Comprehension

Program model linking has been largely overlooked andnot constrained properly in the extraction of software systemmodels. This often results in inaccurate system modelsat different levels of abstraction even if programs can beextracted correctly. This ...
Estimating software component reliability by leveraging architectural models
ICSE '06: Proceedings of the 28th international conference on Software engineering

Software reliability techniques are aimed at reducing or eliminat-ing failures in software systems. Reliability in software systems istypically measured during or after system implementation. How-ever, software engineering methodology lays stress on ...
LabView based experimental validation of fractional order motion controllers
CCDC'09: Proceedings of the 21st annual international conference on Chinese Control and Decision Conference

Fractional calculus has been more and more frequently used in the control domain in recent years. But the fractional order controllers are not widely implemented on the real-time experiments because of the complexity of realization. In this paper, for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ASE '01: Proceedings of the 16th IEEE international conference on Automated software engineering

November 2001

Publisher

IEEE Computer Society

United States

Publication History

Published: 26 November 2001

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chowdhury SShrestha SJohnson TCsallner CRothermel GBae D(2020)SLEMIProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380381(335-346)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380381
Chowdhury SMohian SMehra SGawsane SJohnson TCsallner CChaudron MCrnkovic IChechik MHarman M(2018)Automatically finding bugs in a commercial cyber-physical system development tool chain with SLforgeProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180231(981-992)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180231
Elberzhager FRosbach ABauer TCarrozza GPietrantuono RManetti V(2013)Analysis and testing of matlab simulink models: a systematic mapping studyProceedings of the 2013 International Workshop on Joining AcadeMiA and Industry Contributions to testing Automation10.1145/2489280.2489285(29-34)Online publication date: 15-Jul-2013
https://dl.acm.org/doi/10.1145/2489280.2489285
Chen CSun JLiu YDong JZheng M(2012)Formal modeling and validation of Stateflow diagramsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-012-0235-014:6(653-671)Online publication date: 1-Nov-2012
https://dl.acm.org/doi/10.1007/s10009-012-0235-0
Owen DDesovski DCukic BMayer JMerkel R(2006)Random testing of formal software models and induced coverageProceedings of the 1st international workshop on Random testing10.1145/1145735.1145739(20-27)Online publication date: 17-Jul-2006
https://dl.acm.org/doi/10.1145/1145735.1145739
Chen CDong J(2006)Applying timed interval calculus to simulink diagramsProceedings of the 8th international conference on Formal Methods and Software Engineering10.1007/11901433_5(74-93)Online publication date: 1-Nov-2006
https://dl.acm.org/doi/10.1007/11901433_5
Tripakis SSofronis CCaspi PCuric A(2005)Translating discrete-time simulink to lustreACM Transactions on Embedded Computing Systems10.1145/1113830.11138344:4(779-818)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1145/1113830.1113834
Paradkar AKlinger T(2004)Automated Consistency and Completeness Checking of Testing Models for Interactive SystemsProceedings of the 28th Annual International Computer Software and Applications Conference - Volume 0110.5555/1025117.1025521(342-348)Online publication date: 28-Sep-2004
https://dl.acm.org/doi/10.5555/1025117.1025521
Caspi PCuric AMaignan ASofronis CTripakis SNiebert PMueller FKremer U(2003)From simulink to SCADE/lustre to TTAProceedings of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems10.1145/780732.780754(153-162)Online publication date: 11-Jun-2003
https://dl.acm.org/doi/10.1145/780732.780754
Caspi PCuric AMaignan ASofronis CTripakis SNiebert P(2003)From simulink to SCADE/lustre to TTAACM SIGPLAN Notices10.1145/780731.78075438:7(153-162)Online publication date: 11-Jun-2003
https://dl.acm.org/doi/10.1145/780731.780754

Abstract

References

Cited By

Recommendations

Resolving Linkage Anomalies in Extracted Software System Models

Estimating software component reliability by leveraging architectural models

LabView based experimental validation of fractional order motion controllers

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations