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

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.