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