Formal Verification in Model Based Development Dependable Computing Incorporated

Format:

Conference/Event

Author/Creator:

Hocking, Hocking, author.

Contributor:

Aiello, M. Anthony

Knight, John C.

Shiraishi, Shin'ichi

Conference Name:

SAE 2015 World Congress & Exhibition (2015-04-21 : Detroit, Michigan, United States)

Language:

English

Physical Description:

1 online resource

Place of Publication:

Warrendale, PA SAE International 2015

Summary:

AbstractSoftware 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

Notes:

Vendor supplied data

Publisher Number:

2015-01-0260

Access Restriction:

Restricted for use by site license