| lesar, ecverif - formal verification |
lesar, ecverif - formal verification
lesar file.lus node [options]
ecverif file.ec [options]
The lesar command first calls lus2ec, then ecverif. The ecverif tool takes a program whose first output is Boolean, and try to prove that this Boolean output remains true, for any execution of the program (i.e. whatever is the infinite sequence of input values received by the program). Moreover, the tool supposes that every assertion (assert statements) appearing in the program denotes an hypothesis on the program environement, so the goal of the tool is at last to prove that:
Whatever the sequence of inputs, as long as the assertions (the hypothesis) are satisfied, the first output (the property) always remains true.
The input program, often called the verification program, is generally built as a combination of the program to validate (the implementation) together with another program (the observer) expressing the safety property. The user may read the Lustre Tutorial which explains how to build verification programs suitable for lesar/ecverif.
ecverif is a model-checker: it explores a finite model (an automaton) of the program. This model is an abstraction that represents an upper-approximation of all the possible executions of the program. The abstraction made on the program is conservative: if the verification suceeds on the model, the property is also satisfied by the program. In this case the tool answer True Property. If the verification fails on the model, the result is inconclusive: either the property is not satisfied by the program, or the property is too complex for the tool. So when the tool answer False Property, it simply means I don't know!
More precisely, the Boolean part of the program is completly reflected in the model, but everything else is abstracted (numerical variables, external types and functions ...). Note that, as a consequence of this, the model-checking is complete for purely Boolean programs (e.g. logical circuits).
Nevertheless, some knowledge on numerical properties has been added to the model checker. A library based on polyhedra manipulation can be used to check whether linear constraints are feasible or not. For instance, using the polyhedra library, the tool will realise that the condition "(y < x) and (0 < e) and (x + 2*e < y)" cannot be satisfied by any numerical values. This information is then taken into account to obtain a more precise model, but note that the verification still remains partial in general.
The successive stages of the computation are involving complex algorithms that may take (a lot of) time. It is recomended to use the verbose mode: in this case ecverif outputs information on the current stage, that allows the user to "guess" if the computation has a chance to end in a reasonable delay. The stages are:
The source code is optimized for the proof: this stage performs dependence checking, syntactic minimisation, and other optimization at the source level. The complexity here is reasonable (linear or quadratic).
The Boolean part of the program is identified and transformed in a set of logical functions, represented by bdds (Binary Decision Diagrams). The result is an implicit representation of the model to check. This stage may be exponential in the worst case.
Several algorithms can be selected. In all cases, the time necessary for the traversal of the model can be exponential in the worst case.
set the verbose mode. Since the algorithms used in the tool are very expensive, it is strongly recomended to use this option in order to have a feed-back on the verification progress.
print available options.
Normally, the first stage of the verification consists in minimizing the source program, according to syntactic equivalence of expressions. This checking also takes into account equivalence of recursive definitions. The result is much more precise than a simple "common sub-expression checking", but indeed more expensive, so the user can disable it with this option.
split the property into several smaller ones (if possible).
force static Boolean optimization of the source program. This option was supported by older versions, but it is (almost) obsolete since the bdds construction stage is now optimized.
The main stage of the model checker consists in exploring the underlying automaton (the model). The user may choose between several algorithms for this exploration.
Assertions are taken into account during the exploration to throw away unfeasible transitions. A state whose all outgoing transitions have all been discarded is said to be a sink state. Assertions that can produce sink states are said to be non-causal.
(default) use the enumerative algorithm. The automaton is checked state by state, starting from the initial one. The verification fails as soon as a state violating the property is reached. An error occurs if the assertions are found to be non-causal.
only works in enumerative mode. The exploration stops after n states are visited.
use the symbolic forward algorithm. The set of reachable states is build as a Boolean formula over the state variables. The verification fails if this set contains states violating the property.
use the symbolic backward algorithm. This algorithm builds a symbolic representation of the bad states, i.e. states that can lead to the violation of the property. The verification fails if the initial state belongs to this set.
compute a causal assertion equivalent to the initial one, before starting the model-checking. This computing is expensive, so it is recommended to use it only when needed (when a first attempt have failed because of non-causal assertions). Moreover, this option must not be used with the forward algorithm, which implements its own treatment for non-causal assertions.
force the model checker to use the polyhedra library to check wether linear constraints on numerical values are feasible. Without this option, semantics of numerical values is completly ignored, and any condition is supposed to be feasible as soon as integers or reals are involved.
print a diagnosis when verification fails. The diagnosis is a sequence of input values that may leads to a state violating the property.
Due to abstractions applied to non-boolean programs, the counter-examples produced by the -diag option are not always very useful, mainly because (1) new inputs are created to the model to take into account the (now unpredicatable) non-boolean elements of the program, and (2) as already explained, abstraction may lead to false negatives: counter-examples, which have no counterpart in the concrete model. In general, associating a long and complex abstract counter-example with a concrete one is a long and tedious exercise. This option generates richer output to the file called filename, which, in turn, can be fed into the tool lurette to try and produce concrete counter-examples automatically.
The lurette file contains three Lustre nodes node_main, node_assertion and node_oracle (where node is the name of the main node in the verified program), which are to be given to lurette as the main, assertion and oracle node respectively. The length of the counter-example produced is reported by lesar. The first (numeric) parameter specifies the minimum length counter-example to produce. Typically, this is set to 0, for the shortest counter-examples, but sometimes the user may wish to force lesar to produce longer counter-examples.
This option automatically enforces -forward.
perform a "clever" variable ordering before building bdds; this option is sometimes useful when the state generation pahse cannot even start.
the space devoted to bdds is allocated by pages. Before allocating new pages, the program first performs garbage collection; for big programs, frequent garbage collection may dramatically slow down the model-checking, so the user may increase the size of pages, expressed in kilo-unit (default 10).
Building verification programs to "feed" lesar is quite hard. The graphical proof manager xlesar can be a simpler way for starting with formal verification.
| lesar, ecverif - formal verification |