Browse Publications Technical Papers 2015-01-0260
2015-04-14

Formal Verification in Model Based Development 2015-01-0260

Software verification is a critical component of software development. Software verification techniques include different forms of testing, inspection, static analysis, and formal verification. Formal verification offers the advantage that it corresponds, at least informally, to testing all possible paths through the software.
There are two primary approaches to using formal verification to establish properties of software: (a) proving properties of a formal specification, and (b) proving an implementation is a refinement of its specification. The first approach allows inference of the proven properties of the implementation provided the implementation is correct. The second approach allows inference of the correctness of the implementation.
Proving properties of a specification provides a means for detecting critical design flaws early in the development process. In model-based development, the model (e.g., a set of SIMULINK diagrams) is a formal specification of the desired system. Thus, formal methods can be applied to such models to gain the advantage of early defect detection.
The technique we have developed begins by synthesizing a formal specification of a SIMULINK model in the PVS specification language. Once the model has been converted to PVS, standard theorems that characterize the basic type and consistency rules of SIMULINK are proved using the PVS verification system.
Once the standard theorems are proved, theorems describing crucial properties (especially those related to safety) of the subject system are stated and proved. To demonstrate the utility and feasibility of our approach, we analyzed a hypothetical ABS controller model, based on a model provided by MathWorks.

SAE MOBILUS

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

Access SAE MOBILUS »

Preview Document Add to Cart
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:
JOURNAL ARTICLE

Code Generation for Safety-Critical Systems – Open Questions and Possible Solutions

2008-01-0385

View Details

TECHNICAL PAPER

In Operation Detection and Correction of Rotor Imbalance in Jet Engines Using Active Vibration Control

941151

View Details

JOURNAL ARTICLE

Efficient Testing Framework for Simulink Models with MTCD and Automated Test Assessments in the Context of ISO 26262

2014-01-0306

View Details

X