Assume-Guarantee Reasoning for Deadlock
Sagar
Chaki, Nishant Sinha,
Proceedings of the 6th International Conference on Formal
Methods in Computer-Aided Design (FMCAD), page 134-141, November
12-16, 2006
Abstract:
We extend the learning-based automated assume guarantee paradigm to
perform compositional deadlock detection. We define Failure Automata,
a generalization of finite automata that accept regular failure
sets. We develop a learning algorithm LF that constructs
the minimal deterministic failure automaton accepting any unknown
regular failure set using a minimally adequate teacher. We show how
LF can be used for compositional regular failure language
containment, and deadlock detection, using non-circular and circular
assume guarantee rules. We present an implementation of our techniques
and encouraging experimental results on several non-trivial
benchmarks.
PDF /
Online
© IEEE