Three Optimizations for Assume-Guarantee Reasoning with L*
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.
PDF /
Online
© Springer