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.
Formal Verification in Model Based Development
Sae Technical Papers
SAE 2015 World Congress & Exhibition ; 2015
2015-04-14
Conference paper
English
Formal Verification for Model-Based Development
SAE Technical Papers | 2005
|Formal verification for model-based development
Automotive engineering | 2005
|Formal verification in model based development
Automotive engineering | 2015
|2005-01-0781 Formal Verification for Model-Based Development
British Library Conference Proceedings | 2005
|