Formal verification in Engee

Formal verification is a mathematical analysis method that makes it possible to fully investigate all possible behaviors of a model with respect to specified properties.

Unlike a conventional simulation, which performs only individual scenarios, formal verification allows us to prove that a certain property of the model is always fulfilled, or to identify a counterexample.

Formal verification complements the model-oriented approach in Engee well: the same model can be used for simulation, code generation, and behavior verification.

Practical implementation in Engee

In the Engee environment, formal verification is implemented through the generation of formal models in the Promela language and their automatic verification using the Spin system.

Promela (PROcess MEta LAnguage) is a language for specification of requirement models or programs.
Spin (Simple Promela INterpreter) — a program that allows:
1. Interpret the model description in Promela language (simulation mode models);
2. Generate from the model description in Promela language and specifications specified by the formula LTL, a C verifier program that allows automatic formal verification of a specification, in particular:
  - Check the invariants specified in the specification;
  - Look for counterexamples if the invariants are not satisfied.

Read more about Promela generation in Engee in the article Generating Promela in Engee.

Formal methods

Formal verification in Engee is based on the idea of a complete study of the behavior of the model.

For example, when creating a model state machine (in the block Chart), its visual diagram itself cannot be checked automatically. Therefore, before launching Spin, the model is transformed into a strictly defined formal description in the Promela language.

It is with this formal representation that Spin works: it mathematically analyzes the model, iterates through possible transition sequences, and verifies that the specified properties (LTL formulas) are fulfilled.

This approach refers to formal methods — methods based on an accurate mathematical description of the behavior of the system. Unlike classical testing, where individual scenarios are tested, formal methods allow you to explore the model completely, without selecting input data and without manually analyzing transitions.

As a result, the Engee model becomes a mathematically rigorous object: all states, variables, and transitions are recorded as Promela code, and Spin examines the entire state space of this formal model and determines whether the specified properties are fulfilled.

Formal models

In Engee, a formal model is created automatically when generating code on Promela. This model describes:

Available variables (global and local);
The structure of states and transitions;
Activation conditions and logic of operation of the Chart blocks;
The order of calculation and the interaction of the model elements.

The formal model should be unambiguous: syntax and semantics do not allow ambiguous interpretations. Thanks to this, the Spin tool can explore the model mathematically accurately and perform strict verification of properties.

Formal analysis

After building a formal model, a formal analysis is performed, a procedure that mathematically verifies whether the model meets the specified properties and requirements.

Formal analysis is verification with a complete search of the model execution options. During the analysis, all possible states and transitions are investigated, providing guaranteed confirmation or refutation of the specified properties.

Properties in formal analysis are verifiable requirements for the model. Each property is formulated as a separate verification case (for example, in the form of an LTL formula). Determining the full set of properties and verifying their implementation allows you to make sure that the behavior of the model is equivalent to the stated requirements.:

If the property turns out to be true, then this guarantees that it is true in all possible scenarios of the model.;
If the property is found to be false, then an additional check is required — usually an analysis of a counterexample.

Relationship to model-based design

Model-based design and formal verification naturally complement each other. A model created in a visual environment (for example, using the Chart blocks) is already a machine-readable description of the system’s behavior.

This allows you to apply formal methods to it directly, without having to manually create separate formal specifications.

When generating Promela from Engee models, the existing structure of blocks, states, and transitions is used, so formal verification becomes a continuation of the usual modeling process. Advantages of this approach:

Errors are detected at the design stage, not in the final stages of testing.;
The traceability between the model, its behavior and formal properties is ensured.;
Verification costs are reduced, as the analysis is performed automatically and does not require the preparation of additional test scenarios.