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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Emmi, M., Giannakopoulou, D., & Pǎsǎreanu, C. S. (2008). Assume-guarantee verification for interface automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5014 LNCS, pp. 116–131). https://doi.org/10.1007/978-3-540-68237-0_10
Mendeley helps you to discover research relevant for your work.