Assume-Guarantee Verification for Interface Automata

Michael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu

Interface automata provide a formalism for capturing the high level interactions between the components of a software system. Checking component compatibility and other safety properties in a system expressed in terms of interface automata suffers from scalability issues that are inherent in exhaustive techniques such as model checking. To address this issue, this work develops a theoretical framework and automated algorithms based on learning for assume guarantee verification of interface automata. We propose sound and complete assume-guarantee rules for interface automata and learning-based algorithms that automate assume-guarantee reasoning for interface automata based on the defined rules. Our algorithms have been implemented in the LTSA tool and have been applied to a realistic case study.