Compositional Verification

 Objectives

We focus on the following challenging problems:

• Scalability that avoids the state space explosion problem and therefore allows increasing the size of systems that can be verified.
• Effectiveness that permits to detect as early as possible errors of systems models in the design phase.
• Compositionality that allows inferring global properties of a system from the known local properties of its components.
• Incrementality that integrates verification into the design process and therefore allows detecting an error as soon as it appears. The incrementality also permits to reused intermediate verification steps that reduces verification costs.

 Main results

• Compositional verification: For a given safety property, the method consists in iteratively conjoining the predicate characterizing violations of the property (set of bad states) with an over-approximation of the set of reachable states. If the conjunction is false, then the property is guaranteed. Otherwise, there is a (bad) state within the approximation that violates the property.

• Efficient computation of invariants: The over-approximation is the conjunction of two kinds of invariants: component invariants (CI) and interaction invariants (II). We provide efficient methods for computing the two kinds of invariants. CIs express local constraints of atomic components and are generated by simple forward analysis of their behavior. These are over-approximations of the set of their reachable states. IIs characterize constraints on the global state space induced by synchronizations between components. They are computed on compositional abstractions of the global system.

• Checking reachability: To eliminate remaining false positives, a compositional abstraction refinement approach is developed. It is based on an abstraction of the components to Boolean systems and subsequent generation of inductive invariants and pre-image computation. Result of this final step of verification is an error trace that proves and demonstrates the reachability of a found bad state.

• Incremental verification: We also provide incremental construction and verification methods which are based on a construction process leading to a composite component through a sequence of constituent components. We study rules which allow preserving established invariants during the incremental construction. For the general case where a system might not satisfy these rules, we propose methods for computing incrementally invariants of the entire system from the established invariants of its constituents.

The experimental results on large-scale and complex systems show the efficiency of our verification method.

 D-Finder tool-set

The methodology has been implemented in the BIP D-Finder toolset for compositional and incremental deadlock detection and verification. D-Finder consists of the following modules:

• Component invariant generation: generates automatically component invariants by computing the predicates attached to control locations. These predicates are satisfied whenever the component reaches the corresponding control location. DIS generation: taking the set of system interactions as the input, DIS generation module implements the method to compute a set of states from which all those interactions are disabled by computing the disabled condition of each transition involved in the interaction.

• Abstraction: this module implements a method for computing abstract system from a concrete one based on the predicates attached to control locations of components.

• Interaction invariant generation: this module computes, from the abstract system, interaction invariants. Both global and incremental computation methods of interaction invariants were implemented in this module. The interactions invariants of the concrete system are obtained by concretizing the abstract ones.

• Satisfiability: satisfiability module checks the satisfiability of a formula by using Cudd package if the formula contains only boolean variables or by using an external SAT-Solver tool Yices otherwise. If the given formula is not satisfiable, it returns a false output. Otherwise, it returns a true output with all the solutions satisfying the formula.

• CEX generation: Counter example generation to verify the reachability of possible deadlocks and provide help to understand the causes of an error. Currently, counter examples can be generated for Boolean systems with BDD based pre- post-image computation.

• Predicate abstraction: Abstraction method to reduce systems with integer data to Boolean systems. Predicate abstraction is performed localy on each component in solation using the guards as initial predicates. The method preserves the set of disables states. The resulting system can be used for further steps like deadlock and counter example analysis.

• Feasibility check: Counter examples on systems that were generated by predicate abstraction, might not be feasible on the concrete system. The feasibility check analyses if the trace can be performed on the concrete system and reports if there is a conflict.

 Publications

• Incremental Component-based Construction and Verification using Invariants, S. Bensalem, M. Bozga, A. Legay, T-H. Nguyen, J. Sifakis and R. Yan, in FMCAD 2010.

• Incremental Invariant Generation for Compositional Design, S. Bensalem, A. Legay, T-H. Nguyen, J. Sifakis and R. Yan, in TASE 2010.

• Compositional Verification for Component-based Systems and Application, S. Bensalem, M. Bozga, T-H. Nguyen, J. Sifakis, IET Software Journal, Special Issue on Automated Compositional Verification, Volume 4, Issue 3, p. 181-193 (June 2010).

• “Rock Solid” Software: A Verifiable and Correct-by-Construction Controller for Rover and Spacecraft Functional Levels, Saddek Bensalem, L. de Silva, M. Gallien, F. Ingrand, R. Yan, in ISAIRAS 2010.

• D-Finder: A Tool for Compositional Deadlock Detection and Verification, S. Bensalem, M. Bozga, T-H. Nguyen and J. Sifakis, in CAV 2009.

• Toward a More Dependable Software Architecture for Autonomous Robots, S. Bensalem, M. Gallien, F. Ingrand, I. Kahloul and T-H. Nguyen, Special issue on Software Engineering for Robotics of the IEEE Robotics and Automation Magazine, Volume 16, Issue 1, p. 67-77 (March 2009).

• Compositional Verification for Component-based Systems and Application, S. Bensalem, M. Bozga, T-H. Nguyen, J. Sifakis, in ATVA 2008.

• Incremental Component-Based Construction and Verification of a Robotic System, A. Basu, M. Gallien, C. Lesire, T-H. Nguyen, S. Bensalem, F. Ingrand, J. Sifakis, in ECAI 2008.

 Case studies

The table below gives an overview of the results obtained on several benchmarks. The signification of columns is as follows: comp — the number of BIP components in the example, inters — number of interactions, locs — the overall number of control locations, b (resp int) — the overall number of boolean (resp. integer) variables, dls — the number of potential deadlocks, time — the total verification time in m:s and mem — the total memory usage in Mb.

Verification of the modules in Dala Robot

 Download

The D-Finder tool-chain can be downladed here.

 People involved

• Joseph Sifakis, CNRS Research Director, Verimag.

• Saddek Bensalem, Professor, Joseph Fourier University, Verimag.

• Marius Bozga, CNRS Research Engineer, Verimag.

• Andreas Griesmayer, Post-doc, Verimag.

• Axel Legay, Researcher, IRISA, Rennes.

• Ouri Maler, Engineer, Verimag.

• Thanh-Hung Nguyen, Verimag.

• Rongjie Yan, Post-doc, Verimag.