Sagar Chaki

Sagar Chaki, Ofer Strichman, Formal Methods in System Design (FMSD), volume 32, number 3, page 267-284, June 2008.

Abstract: The learning-based automated Assume-Guarantee reasoning paradigm has been applied in the last few years for the compositional verification of concurrent systems. Specifically, L* has been used for learning the assumption, based on strings derived from counterexamples, which are given to it by a model-checker that attempts to verify the Assume-Guarantee rules. We suggest three optimizations to this paradigm. First, we derive from each counterexample multiple strings to L*, rather than a single one as in previous approaches. This small improvement saves candidate queries and hence model-checking runs. Second, we observe that in existing instances of this paradigm, the learning algorithm is coupled weakly with the teacher. Thus, the learner completely ignores the details of the internal structure of the system and specification being verified, which are available already to the teacher. We suggest an optimization that uses this information in order to avoid many unnecessary membership queries (it reduces the number of such queries by more than an order of magnitude). Finally, we develop a method for minimizing the alphabet used by the assumption, which reduces the size of the assumption and the number of queries required to construct it. We present these three optimizations in the context of verifying trace containment for concurrent systems composed of finite state machines. We have implemented our approach in the ComFoRT tool, and experimented with real-life examples. Our results exhibit an average speedup of between 4 to 11 times, depending on the assume-guarantee rule used and the set of activated optimizations.