Benoit Boyer, Saddek Bensalem, Marius Bozga and Axel Legay
Incremental Generation of Linear Invariants for Component-Based Systems (2012)
Incremental Generation of Linear Invariants for Component-Based Systems (2012)
TR-2012-15.pdf
Keywords: invariant generation, linear invariant, incremental verification, comp onent-based systems
Abstract: Linear invariant generation has been intensively considered as an effective verification method for concurrent systems. However, none of the existing work on the topic strongly exploits the structure of the system and the algebra that defines the interactions between its components. This not only has an impact on the computation time, but also on the scalability of the method. In a series of recent work, we developed an incremental approach for generating boolean invariants for systems described in the BIP component framework. BIP is an expressive modeling formalism including a rich algebra to describe component interactions. The objective of this paper is to extend and propose new techniques dedicated to the computation of linear interactions invariants, i.e., invariants that are described by linear constraints and that relate states of several components in the system. In particular, we propose an incremental approach that allows to discover and reuse invariants that have already been computed on subparts of the model. Those new techniques have been implemented in D-FINDER, a tool for checking deadlock freedom on BIP systems using invariants, and evaluated on several case studies. The experiments show that our approach outperforms classical techniques on a wide range of models.
