Model Verifier     


Ronen Levy photo Natalia Razinkov photo

Model Verifier - overview

Formal Verification for UML and SysML ,the project's goal is to develop industrial-strength formal verification (FV) capabilities for the systems engineering community. In particular, we target safety critical and high integrity systems, for which correct functionality is essential. As the size and complexity of these systems grows a real need for automated verification tools has arisen. Whether it is in the aerospace, defense, automotive, or medical domain, the development of such systems is governed by strict standards. Modern standards, such as Do-178C, now advocate the use of formal methods, making the developers' need for such tools more pronounced.

An FV engine answers the question "does the system adhere to its correctness property"? A positive answer is based on a mathematical proof and means that this property is true on all possible behaviors of the system, under any possible environment input. In case of a negative answer, the formal verification engine will supply a specific scenario of environment inputs and system response in which the correctness property is violated. This is achieved by an exhaustive mathematical analysis, as opposed to testing, which only samples the space of possible behaviors.

Formal verification is successfully used for verifying hardware designs. We aim at extending its applicability to system models. Given a UML/SysML behavioral model we verify properties of its behavior. The tool is meant to be used by system engineers, who are not experts in logics and do not have experience with formal verification. To make it easy to use, we supply predefined template properties. These include well understood concepts such as mutual-exclusion and deadlock. However, verification experts can exploit the full power of FV technology via temporal specification languages.

The project implements the above ideas through a Rhapsody plug-in. The input is a UML/SysML model using state diagrams to describe components' behavior. Correctness properties specify what the user wishes to verify on the design. By simply clicking a button an automatic check is launched and the user is presented with the results – either pass or fail. If the design fails to meet the specified correctness property a sequence diagram is generated, showing a specific scenario that contradicts the property.

We envision our FV tool being used in a model-driven development flow. This technology can be extremely useful on high-level models of the system. At this stage the behavioral content describes modes of operation, willingness to engage in transactions, handling of hazardous situations, restrictions on interfaces, etc.

Finding design and reasoning flaws at this early stage enables making major changes to the design, which if found later would be expensive if not impossible. On the other hand, the same technology can be exploited for verifying implementation-level models to verify the actual functional correctness of specific system components. This is particularly important when automatic code generation is used.

A third use case is for critical protocols or procedures, in which case a model is created for the specific purpose of verifying its behavior. We believe state-machines are more intuitive and suitable for such modeling, when compared to hardware or software languages.