This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Case Study of Commercially Available Tools that Apply Formal Methods to a Matlab/Simulink/Stateflow Model
Technical Paper
2004-01-1765
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
This paper will apply a number of commercially available formal methods tools to discrete Matlab models and will report these results. After introducing formal methods, the features and ease of use of each tool will be reported as well as describing how this will benefit the end user. The tools evaluated include Reactive System's Validator and TNI-Valiosys' SCB blockset. One other tool was evaluated, but the tool vendor asked to have the results removed from the paper.
With the ever-increasing complexity of embedded software applications, and the emergence of more and more safety-critical applications, thorough validation and verification is needed. To address this need, many embedded software development groups are using models and doing upfront engineering before testing the final product. [3] Using the old style of testing late in the development cycle resulted in long and expensive release cycles. Ford estimated that 60% of work tasks were to correct requirements or design defects that had been released to downstream developers [2]. With today's increasing need to get to market quickly with a safe product, this old style of testing is not adequate, and a new technology such as formal methods is needed to address the issues.
Recommended Content
| Technical Paper | WinSPEED Digital Audio Development System |
| Technical Paper | An Integrated Tool Set For Developing Embedded Control System Software |
| Technical Paper | Best Practices and Recommendations for the Model-Based Development Process |
Authors
Citation
Ranville, S., "Case Study of Commercially Available Tools that Apply Formal Methods to a Matlab/Simulink/Stateflow Model," SAE Technical Paper 2004-01-1765, 2004, https://doi.org/10.4271/2004-01-1765.Also In
In-Vehicle Networks and Software, Electrical Wiring Harnesses, and Electronics and Systems Reliability
Number: SP-1852; Published: 2004-03-08
Number: SP-1852; Published: 2004-03-08
References
- Toeppe, S. Ranville, S. “An Automated Inspection Tool For a Graphical Specification and Programming Language” 1999 Quality Week Conference
- Patel, S. Smith, P. Sun, W. Ramanan, R. Donald, H. Toeppe, S. Ranville, S. Bostic, D. Butts, K. “CACSD in Production Development: An Engine Control Case Study” 2000 Global Powertrain Conference
- Ranville Scott Black Paul E. “Automated Testing Requirements - Automotive Perspective” The Second International Workshop on Automated Program Analysis, Testing and Verification May 2001 Toronto
- Boehm, Barry Software Engineering Economics Englewood Cliffs,NJ Prentice-Hall, Inc. 1981
- Blackburn, M.R. Busser R.D. Nauman A.M. Knickerbocker R., Kasuda R. Mars Polar Lander Fault Identification Using Model-based Testing Proceeding in IEEE/NASA 26th Software Engineering Workshop November 2001
- http://mars.jpl.nasa.gov/msp98/lander/fact.html