Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning

Finite-state verification techniques are often hampered by the stateexplosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. Using recent advances in assume-guarantee reasoning that automatically generate assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks, we evaluated the decompositions as the systems were scaled. In only a few cases could assume-guarantee reasoning verify properties on larger systems than monolithic verification and, in these cases, assumeguarantee reasoning could only verify these properties on systems a few sizes larger than monolithic verification. This discouraging result, although preliminary, raises doubts about the usefulness of assume-guarantee reasonin...

• Type: Conference
• Year: 2006
• Where: ISSTA
• Authors: Jamieson M. Cobleigh, George S. Avrunin, Lori A. Clarke
• Keywords: Assume-guarantee Reasoning, Finite-state Verification Techniques, ISSTA 2006, Monolithic Verification