Assume-Guarantee Tools for Component-Based Software Verification

This paper presents a minimized assumption generation method and its associated tools for L*-based assume-guarantee verification of component-based software by model checking. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. In the proposed method, a verification target is decomposed into components so that we can model check each of them separately. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. Our experience so far indicates that the implemented tools are potential for verifying practical component-based software.