Assume-Guarantee Verification for Interface Automata

Interface automata provide a formalism capturing the high level interactions between software components. Checking compatibility, and other safety properties, in an automata-based system suffers from the scalability issues inherent in exhaustive techniques such as model checking. This work develops a theoretical framework and automated algorithms for modular verification of interface automata. We propose sound and complete assume-guarantee rules for interface automata, and learning-based algorithms to automate assumption generation. Our algorithms have been implemented in a practical model-checking tool and have been applied to a realistic NASA case study.

• Type: Conference
• Year: 2008
• Where: FM
• Authors: Michael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu
• Keywords: Algorithms, FM 2008, Formal Methods, Interface Automata, Realistic Nasa Case