Automated Assume-Guarantee Reasoning for Simulation Conformance
Sagar
Chaki, Edmund Clarke, Nishant Sinha, Prasanna Thati,
Proceedings of the 17th International Conference on Computer
Aided Verification (CAV), LNCS 3576, page 534-547, July 6-10,
2005
Abstract:
We address the issue of efficiently automating assume-guarantee
reasoning for simulation conformance between finite state systems and
specifications. We focus on a non-circular assume-guarantee proof
rule, and show that there is a weakest assumption that can be
represented canonically by a deterministic tree automata (DTA). We
then present an algorithm LT that learns this DTA
automatically in an incremental fashion, in time that is polynomial in
the number of states in the equivalent minimal DTA. The algorithm
assumes a teacher that can answer membership and candidate queries
pertaining to the language of the unknown DTA. We show how the teacher
can be implemented using a model checker. We have implemented this
framework in the ComFoRT toolkit and we report encouraging results
(over an order of magnitude improvement in memory consumption) on
non-trivial benchmarks.
PDF /
Online
© Springer