Introduction |

**NBAC** is a verification/slicing tool developped during my PhD
thesis at the laboratory VERIMAG, part of IMAG federation in Grenoble.
Its developpement has been since I got my position at IRISA.

The tool analyses synchronous and deterministic reactive systems containing combination of Boolean and numerical variables and continuously interacting with an external environment. Its input format is directly inspired by the low-level semantics of the LUSTRE dataflow synchronous language. Notice that asynchronous and/or non-deterministic systems can be compiled in this model. The following connections are shown below.

The kind of analyses performed by **NBAC** are

**Reachability analysis**from a set of initial states, which allows to compute invariants satisfied by the system;**Coreachability analysis**from a set of final states, which allows to compute sets of states that may lead to a final state;**Combination of the above analysises**, which allows to either verify invariance or more generally safety properties, either to slice a system, i.e., to compute (an overapproximation of) sets of states belonging to executions starting in an initial state and leading to a final state.

together with a necessary condition on states and inputs to stay in this set during an execution, either a verdict to a verification problem. The returned set of states and necessary condition is actually given by an explicit control structure, where locations are labeled by (disjoint) sets of states and transitions between locations are labeled by necessary conditions.

The tool has been developped mainly in OCaml. For representing Boolean functions and guarded functions, it uses the BDD library Cudd, an extension to it called Cuddaux,which are both interfaced to OCaml with MLCuddIDL. The tool uses now the APRON for the numerical abstrac domain, instead of the older version of the convex polyhedra library NewPolka

It can be downloaded in binary format for Linux and Solaris systems. A tutorial is available, as well as a user manual.

The tool is founded on the theory of abstract interpretation
[2][3][4], which allows to overcome the
undecidability of the reachability/coreachability problem for the
class of program treated by **NBAC**. Sets of states are
represented in an approximate way by abtract values belonging to an
abstract domain, and (fixpoint) computations are performed on this
abstract domain. This leads to conservative results: if a state is
shown unreachable (resp. not coreachable), then it is for sure. That's
all that can be said.

The "basic" abstract domain we use is the direct product of the
Boolean lattice and the convex polyhedra lattice. More
practically a set of states is represented by the conjunction of a BDD
(for the Boolean variables of the program) and a convex polyhedra (for
its numerical variables).^{1}

The originality of **NBAC** is summarized below:

- Using a single abstract value would lead to very unprecise
results. The tool works actually with an explicit control
structure, defined by a partitioning of the state space. This allows
to represent a global set of states as a finite union of abstract
values, instead of a single asbtract value. The first feature of
**NBAC**is to use a very general notion of control structure in order to to tune very precisely the tradeoff bewteen precision and efficiency of the analyses.^{2}^{3} - The second feature of
**NBAC**is the ability to dynamically refine the control structure, and to guide this refinement by the needs of the analysis. The initial control structure is either provided by the user, either generated by the tool (in which case it is very abstract). Its (successive) refinements followed by analyses allows to improve the accuracy of the results and to incrementally remove states which have already been shown unreachable and/or not coreachable. - In the same goal of adjusting incrementally the tradeoff bewteen
precision and efficiency,
**NBAC**offers as a third feature sophisticated methods for computing postconditions and preconditions of abstract values by the transition function of the program. This has been proven to be "decisif" on the efficiency of the global method.

Details can be found in [10][7][9][8].

Bertrand Jeannet, February 10, 2011

Introduction |