Browse Publications Technical Papers 2004-01-1765

Case Study of Commercially Available Tools that Apply Formal Methods to a Matlab/Simulink/Stateflow Model 2004-01-1765

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.


Subscribers can view annotate, and download all of SAE's content. Learn More »


Members save up to 16% off list price.
Login to see discount.
Special Offer: Download multiple Technical Papers each year? TechSelect is a cost-effective subscription option to select and download 12-100 full-text Technical Papers per year. Find more information here.
We also recommend:

A Software Engineering Framework for Electronic Engine Controllers


View Details


Experiences of Civil Certification of Multi-Core Processing Systems in Commercial and Military Avionics, Integration Activities, and Analysis


View Details


A Systems Engineering Approach to Requirements Elicitation and Management


View Details