Browse Publications Technical Papers 2015-01-0260

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.


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


Members save up to 18% 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:

“Dynamic Analysis of Cabin Tilting System of Heavy Trucks Using ADAMS-View for Development of a Software Interface for Optimization”


View Details


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


View Details


Advances in Automated Inspection Using Contactless Head Height and Countersink Measurement Techniques


View Details