Formal verification in Engee
Formal verification is a mathematical method of analysis that allows you to fully investigate all possible behaviors of the model with respect to specified properties.
Unlike the usual simulation, which performs only individual scenarios, formal verification allows us to establish conclusively that a certain property of the model is always fulfilled, or to identify a counterexample.
Formal verification complements the model-oriented approach well in Engee The same model can be used for simulation, code generation, and behavior property verification.
Practical implementation in Engee
In the environment Engee 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) - the language of specification of requirements models or programs.
-
Spin (Simple Promela INterpreter) — a program that allows:
-
Interpret the model description in Promela language (simulation mode models);
-
Generate from the description of the model in the Promela language and specifications specified by the formula LTL, verifier program in the C language, which allows performing automatic formal verification of the specification, in particular:
-
Check the invariants specified in the specification;
-
Look for counterexamples if the invariants do not hold.
-
-
Learn more about generating Promela in Engee read the article Promela generation in Engee.
Formal methods
Formal verification in Engee It is based on the idea of a complete study of the behavior of the model.
For example, when a model is created state machine (in the block Chart), its visual diagram by itself cannot be checked automatically. Therefore, before launching Spin, the model is converted 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 sequences of transitions and checks the fulfillment of the specified properties (LTL formulas).
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 model Engee It becomes a mathematically rigorous object: all states, variables and transitions are fixed in the form of 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 The formal model is created automatically when generating code on Promela. Such a model describes:
-
Available variables (global and local);
-
The structure of states and transitions;
-
Activation conditions and block operation logic Chart;
-
The order of calculation and interaction of model elements.
The formal model should be unambiguous: syntax and semantics do not allow ambiguous interpretations. Thanks to this, the Spin tool can examine the model mathematically accurately and perform strict verification of properties.
Formal analysis
After the formal model is constructed, formal analysis is performed - a procedure that mathematically checks whether the model meets the specified properties and requirements.
Formal analysis is a verification with a complete search of the execution options of the model. 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 checking their implementation allows you to make sure that the behavior of the model is equivalent to the stated requirements:
-
If the property turned out to be true, then this guarantees its truth in all possible scenarios of the model;
-
If the property is found to be false, then an additional check is required — usually a counterexample analysis.
Connection with model-oriented design
Model-oriented design and formal verification naturally complement each other. A model created in a visual environment (for example, with the usage of Chart blocks) is already a machine-readable description of the behavior of the system.
This allows you to apply formal methods to it directly — without having to manually create separate formal specifications.
When generating Promela from models Engee 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;
-
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.