Introduction

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 model of analyzed systems.

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.

Tasks performed by the tool.

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.

Implementation.

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.

Foundations of the tool.

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).¹

The originality of NBAC is summarized below:

1. 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}
2. 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.
3. 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].

Connection of NBAC with various formats and tools.

Introduction