NBAC Tutorial |

Let us describe a very simle (and maybe stupid) example. We would like to analyse the system depicted on the following figure, where two counters are alternatively incremented.

state b0,b1: bool; x,y : int; transition b0' = not b1; b1' = b0; b2' = b2 xor (b0 and b1); x' = if (b0 = b1) then x+1 else x; y' = if (b0 <> b1) then y+1 else y; initial not b0 and not b1 and x=0 and y=0;

Here we have state variables, but no input variables, as there is no
interaction with an environment. Suppose now we want to check that `x`

is always greater than or
equal to `y`

. We add the declaration

final not (x>=y);

Actually, for some reasons we will explain later, we prefer to "delay" the initial and final sets of states, using a Boolean variable as follows. This gives the program:

state init,ok : bool; b0,b1: bool; x,y : int; transition init' = false; ok' = if init then true else ok and x>=y; b0' = if init then false else not b1; b1' = if init then false else b0; x' = if init then 0 else if (b0 = b1) then x+1 else x; y' = if init then 0 else if (b0 <> b1) then y+1 else y; initial init; final not init and not ok;

Our system corresponds now to the automaton

Let now ask the tool to perform a step of slicing analysis with the command `nbacg example1.ba -analysis 2 -print "+p +a +r"`

The option `-analysis 2` indicates we want to perform slicing or
verification, the option `-print "+p +a +r"` indicates
we want to have information about initial control analysis (`+a`) and
refinement (`+r`).

- Syntaxical analysis - Transformation to BDDs - Treatement of definition of - Treatement of equation of ok init y x b1 b0 - Treatement of formula: assertion initial final - Simplification by careset Variable reordering done Variable reordering done - Simplification by Boolean slicing (reach/coreach) Variable reordering done Forward analysis (.....) Backward analysis (..) Variable reordering done [ v = 0, etiq = control=!ok^!init; def=(true, 1>=0); cube=true , succ = [], pred = [2], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [2], pred = [], v = 2, etiq = control=ok^!init; def=(true, 1>=0); cube=true , succ = [0; 2], pred = [1; 2], ] [ (1,2), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (2,0), bassert=y>=x+1; cube=y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (2,2), bassert=!y>=x+1; cube=!y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (3 vertices, 3 edges, 1.00 e/v, dev(succ/v) = 0.82 dev(pred/v) = 0.82 postpre : (0.00 prod, 2.00 ite, 1.00 inter, 3.00 dec))

First of all, **NBAC** parses the input file and transform all
the expressions into BDDs and MTBDDs. It simplifies the formula by taking into account a careset, which represent the knowledge that some numerical constraints implies other ones. Typically, the fact that

is taken into account in the careset.

Then a Boolean slicing is performed: here only the behaviour of Boolean state variables is analysed. Numerical constraints of the involved formula are just viewed as Boolean inputs however constrained by the careset. A partial knowledge about the numerical domain is then taken into account, but in static way: there is no analysis of the dynamic behaviour of numerical variables during an execution at that step.

At last, **NBAC** build the initial control structure displayed
above, with its graphical representation below.

The control structure here is generated by the tool by exactly
partitioning the current state space (after Boolean slicing) into
initial, final, and other states, and then using a (set of)
location(s) to represent each equivalence class. The advantage of
using two Boolean variables `init` and `final` is to
ensure that one location is enough to excatly the set of initial
states. Otherwise, we have to decompose these sets in an exact union
of abstract values.

Now **NBAC** performs a first reachability analysis:

*** Analysis *** [ v = 0, etiq = control=!ok^!init; def=(true, 1>=0); cube=true , succ = [], pred = [2], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [2], pred = [], v = 2, etiq = control=ok^!init; def=(true, 1>=0); cube=true , succ = [0; 2], pred = [1; 2], ] [ (1,2), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (2,0), bassert=y>=x+1; cube=y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (2,2), bassert=!y>=x+1; cube=!y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (3 vertices, 3 edges, 1.00 e/v, dev(succ/v) = 0.82 dev(pred/v) = 0.82 postpre : (0.00 prod, 2.00 ite, 1.00 inter, 3.00 dec)) *** End of analysis in 5 iterations *** *** narrowing *** *** End narrowing in 1 iterations without stabilization *** *** Analysis *** [ v = 0, etiq = control=!ok^!init; def=(true, y>=x,y<=x+2,y+x>=2); cube=true , succ = [2], pred = [], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [], pred = [2], v = 2, etiq = control=ok^!init; def=(true, y>=0,1>=0,y<=x+1,x>=0); cube=true , succ = [1; 2], pred = [0; 2], ] [ (0,2), bassert=y>=x+1; cube=y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (2,1), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (2,2), bassert=!y>=x+1; cube=!y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (3 vertices, 3 edges, 1.00 e/v, dev(succ/v) = 0.82 dev(pred/v) = 0.82 postpre : (0.00 prod, 2.00 ite, 1.00 inter, 3.00 dec))

The initial control structure is displayed once again. After end of analysis and narrowing, the resulting control structure is displayed, however in a transposed way (it is made ready for a backward analysis). Let us depict in graphically in the right orientation:

*** End of analysis in 4 iterations *** *** narrowing *** *** End narrowing in 1 iterations with stabilization *** *** Refinement *** [ v = 0, etiq = control=!ok^!init; def=(true, y>=x,y<=x+2,y+x>=2); cube=true , succ = [], pred = [2], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [2], pred = [], v = 2, etiq = control=ok^!init; def=(true, y<=x+1,1>=0,x>=0,y>=0); cube=true , succ = [0; 2], pred = [1; 2], ] [ (1,2), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (2,0), bassert=y>=x+1; cube=y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (2,2), bassert=!y>=x+1; cube=!y>=x+1; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (3 vertices, 3 edges, 1.00 e/v, dev(succ/v) = 0.82 dev(pred/v) = 0.82 postpre : (0.00 prod, 2.00 ite, 1.00 inter, 3.00 dec))

The analysis didn't bring us new information, so the control structure remains unchanged. So a refinement is needed, in order to improve the precision of the analysis.

cfc=[[]; [1]; [2]; [0]] refine_cfc forward vertex 2, mset=[(b1,1); (b0,1); (y>=x+1,3)] vertex 0, mset=[] result = [2 => y>=x+1;] *** Analysis *** [ v = 0, etiq = control=!ok^!init; def=(true, y>=x,y<=x+2,y+x>=2); cube=true , succ = [], pred = [2], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [3], pred = [], v = 2, etiq = control=ok^!init; def=(true, y=x+1,1>=0,y>=1); cube=y>=x+1 , succ = [0], pred = [3], v = 3, etiq = control=ok^!init; def=(true, y<=x,1>=0,y>=0); cube=!y>=x+1 , succ = [2; 3], pred = [1; 3], ] [ (1,3), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (2,0), bassert=true; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (3,2), bassert=!b1^b0 + b1^!b0; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (3,3), bassert=true; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (4 vertices, 4 edges, 1.00 e/v, dev(succ/v) = 0.71 dev(pred/v) = 0.71 postpre : (0.00 prod, 1.50 ite, 1.00 inter, 2.50 dec))

Let us perform a forward analysis:

*** End of analysis in 5 iterations *** *** narrowing *** *** End narrowing in 1 iterations with stabilization *** *** Analysis *** [ v = 0, etiq = control=!ok^!init; def=(!b1^b0 + b1^!b0, y=x,1>=0,y>=1); cube=!y>=x+1 , succ = [2], pred = [], v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [], pred = [3], v = 2, etiq = control=ok^!init; def=(!b1^!b0 + b1^b0, y=x+1,x>=0,1>=0); cube=y>=x+1 , succ = [3], pred = [0], v = 3, etiq = control=ok^!init; def=(true, y<=x,1>=0,y>=0); cube=!y>=x+1 , succ = [1; 3], pred = [2; 3], ] [ (0,2), bassert=!b1^!b0 + b1^b0; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (2,3), bassert=!b1^b0 + b1^!b0; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (3,1), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (3,3), bassert=true; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (4 vertices, 4 edges, 1.00 e/v, dev(succ/v) = 0.71 dev(pred/v) = 0.71 postpre : (0.00 prod, 1.50 ite, 1.00 inter, 2.50 dec))

which can graphically depicted with:

*** End of analysis in 3 iterations *** *** narrowing *** *** End narrowing in 1 iterations with stabilization *** *** Conclusion *** Success automaton [ v = 0, etiq = control=!ok^!init; def=(!b1^b0 + b1^!b0, y=x,1>=0,y>=1); cube=!y>=x+1 , succ = [], pred = [2], v = 2, etiq = control=ok^!init; def=(!b1^!b0 + b1^b0, y=x+1,x>=0,1>=0); cube=y>=x+1 , succ = [0], pred = [3], v = 3, etiq = control=ok^!init; def=(!b1^b0 + b1^!b0, y=x,x>=0,1>=0); cube=!y>=x+1 , succ = [2; 3], pred = [3], ] [ (2,0), bassert=!b1^!b0 + b1^b0; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; (3,2), bassert=!b1^b0 + b1^!b0; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (3,3), bassert=true; cube=true; dec=(0.00 prod, 3.00 ite, 1.00 inter, 4.00 dec) ; ] (3 vertices, 3 edges, 1.00 e/v, dev(succ/v) = 0.82 dev(pred/v) = 0.00 postpre : (0.00 prod, 2.00 ite, 1.00 inter, 3.00 dec))

At the end, **NBAC** displays some statistics:

2 cycles of analysis, 1 refinements, 1 divisions Total time spent in verification : 0.18 sec Part of it spent in analysis : 0.14 sec Part of it spent in ref. heuristics : 0.01 sec Part of it spent in partition build & ref : 0.03 sec Total time spent in post-pre-conditions : 0.09 sec make : 0.00 sec; assertion : 0.02 sec; apply : 0.07 sec SUCCESS: property proved *** END ***

During the refinement process, you can automatically dump the current control structure to a file in DOT format, see graphviz for details.

If we type the command

and then convert the DOT file into a Poscript file with the following command (part of graphviz package):

we get the following file example1.ps. With the option
`+all`, the control structure is dump between every analysis step (here,
forward analysis followed by a backward analysis). The final automaton being
empty in this case, it is not displayed !

Let us take the same system, but here we want to perform only
reachability analysis. We type the command `nbacg -analysis 0 -o t.ba -print "+a +r -auto 200" example1.ba`

The option `-analysis 0` means reachability analysis, the
option `-print "-auto 200"` increase the maximal size of
control structure which are fully displayed. Last the option
`-o t.ba` indicates that we want to dump the resulting control
structure into the file `t.ba`, in the same format that the
format of `example1.ba`. We get:

... *** Conclusion *** Valid automaton [ v = 1, etiq = control=init; def=(true, 1>=0); cube=true , succ = [6], pred = [], v = 3, etiq = control=b1^b0^ok^!init; def=(true, y=x,x>=1,1>=0); cube=!y>=x+1 , succ = [5], pred = [4], v = 4, etiq = control=!b1^b0^ok^!init; def=(true, y+1=x,x>=1,1>=0); cube=!y>=x+1 , succ = [3], pred = [6], v = 5, etiq = control=b1^!b0^ok^!init; def=(true, y+1=x,x>=2,1>=0); cube=!y>=x+1 , succ = [6], pred = [3], v = 6, etiq = control=!b1^!b0^ok^!init; def=(true, y=x,1>=0,y>=0); cube=!y>=x+1 , succ = [4], pred = [1; 5], ] [ (1,6), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (3,5), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (4,3), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (5,6), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; (6,4), bassert=true; cube=true; dec=(0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec) ; ] (5 vertices, 5 edges, 1.00 e/v, dev(succ/v) = 0.00 dev(pred/v) = 0.63 postpre : (0.00 prod, 0.00 ite, 1.00 inter, 1.00 dec)) 3 cycles of analysis, 3 refinements, 4 divisions Total time spent in verification : 0.26 sec Part of it spent in analysis : 0.11 sec Part of it spent in ref. heuristics : 0.04 sec Part of it spent in partition build & ref : 0.11 sec Total time spent in post-pre-conditions : 0.17 sec make : 0.00 sec; assertion : 0.06 sec; apply : 0.11 sec FAILURE: property not proved *** OUTPUT *** Resulting automaton printed to the file t.ba *** END ***

Here the control structure will be refined as long as the heuristics find refinement criteria, then it stops the analysis. There is no verification goal here, so even once final locations are not reachable any more, the process is still continued. The resulting control structure can be graphically depicted:

If we append the option(s)
`-dot "example1_reach.dot +all"`, and we translate to Postscript with `dot -Tps example1_reach.dot
>example1_reach.ps`, we get this.

As mentioned above, the resulting control structure, after analysis, can be
dumped with the `-o t.ba` option. Unless the option `+success` is set and the verification goal is proved, the resulting
control structure is dumped to the file `t.ba`:

state b1, b0, ok, init : bool; y, x : int; local _cond0, _cond2, _cond4, _cond6, _cond8 : bool; _bdd5, _bdd14, _bdd9, _bdd6, _bdd3, _bdd2, _bdd10, _bdd1, _bdd0, _bdd11, _bdd12, _bdd7, _bdd4, _bdd13, _bdd8 : bool; _int14, _int11, _int12, _int0, _int3, _int13, _int8, _int1, _int9, _int5, _int2, _int6, _int4, _int7, _int10 : int; definition _cond0 = b1; _cond2 = b0; _cond4 = ok; _cond6 = init; _cond8 = y>=x+1; _bdd5 = if b1 then _bdd0 else _bdd3; _bdd14 = if b1 then _bdd0 else _bdd12; _bdd9 = if b0 then _bdd8 else _bdd0; _bdd6 = if ok then _bdd0 else _bdd3; _bdd3 = if init then _bdd0 else not _bdd0; _bdd2 = if init then _bdd0 else not _bdd1; _bdd10 = if b1 then _bdd9 else _bdd0; _bdd1 = if _cond8 then _bdd0 else not _bdd0; _bdd0 = true; _bdd11 = if b1 then _bdd0 else _bdd9; _bdd12 = if b0 then _bdd0 else _bdd8; _bdd7 = if init then _bdd0 else _bdd1; _bdd4 = if b0 then _bdd3 else _bdd0; _bdd13 = if b1 then _bdd12 else _bdd0; _bdd8 = if ok then _bdd7 else _bdd0; _int14 = if b1 then _int12 else _int13; _int11 = if init then _int0 else _int10; _int12 = if b0 then _int9 else _int11; _int0 = 0; _int3 = y+1; _int13 = if b0 then _int11 else _int9; _int8 = x+1; _int1 = y; _int9 = if init then _int0 else _int8; _int5 = if b0 then _int2 else _int4; _int2 = if init then _int0 else _int1; _int6 = if b0 then _int4 else _int2; _int4 = if init then _int0 else _int3; _int7 = if b1 then _int5 else _int6; _int10 = x; transition ok' = _bdd2; init' = not _bdd0; y' = _int7; x' = _int14; b1' = not _bdd4; b0' = not _bdd5; assertion _bdd6; initial _bdd3; final not _bdd6; automaton location init0 : _bdd3; location good0_n8_b1_b0 : not _bdd10; location good0_n8_not_b1_b0 : not _bdd11; location good0_n8_b1_not_b0 : not _bdd13; location good0_n8_not_b1_not_b0 : not _bdd14; edge (init0,good0_n8_not_b1_not_b0) : _bdd0; edge (good0_n8_b1_b0,good0_n8_b1_not_b0) : _bdd0; edge (good0_n8_not_b1_b0,good0_n8_b1_b0) : _bdd0; edge (good0_n8_b1_not_b0,good0_n8_not_b1_not_b0) : _bdd0; edge (good0_n8_not_b1_not_b0,good0_n8_not_b1_b0) : _bdd0;

Doesn't look pretty, isn't it ? This is because we want to keep the concise
form of the internal BDDs/MTBDDs representation. Each reachable BDD/MTBDD node
is declared as a local variable and defined either as a leaf or as a decision
node. This textual format can be replace by Disjunctive Normal Forms by using the option `-o "-bdd"` instead of the default `-o "+bdd"`. Another difference with the initial file is the `automaton` section,
which defines an explicit control structure.

The file `t.ba` is a valid input to **NBAC**.
For instance, we can type `nbacg -analysis 1 t.ba -o t2.ba`

to perform a coreachability analysis after this reachability analysis.

There is a way to prevent **NBAC** to refine too much the control structure. If we type `nbacg -analysis 0 -o t.ba -partition "-maxloc 4" example1.ba`

we ask **NBAC** to stop refinement as soon as the current control
structure has at last 4 locations.

Conversely, if we want to perform a coreachability analysis, which compute the
set of states that may lead to a final state, we type the command `nbacg
-analysis 1 -o t.ba -dot "example1_coreach.dot +all" example1.ba`
and we obtain this.

Bertrand Jeannet, February 10, 2011

NBAC Tutorial |