Proof Slicing with Application to Model Checking Web Services

Web Services emerge as a new paradigm for distributed computing. Model checking is an important verification method to ensure the trustworthiness of composite WS. abstraction and counterexample driven refinement are major techniques for model checking software and WS. In most of the literature, the refinement is governed by the n of the abstraction. In this paper, we present an innovative technique to distribute the precision information among proof slices, which can be selectively reused by future proofs and hence improve the performance by reducing excessive invocations of theorem provers. Moreover, the reuse approach is flexible for virtually arbitrary future extension. Our theoretical framework subsumes several exbstraction-based model checking techniques, e.g., traction. Besides the correctness and termination proofs, we also conducted theoretical analysis on the performance of the proof slicing algorithm.

• Type: Conference
• Year: 2005
• Where: ISORC
• Authors: Hai Huang, Wei-Tek Tsai, Raymond A. Paul
• Keywords: ISORC 2005, Model Checking, Model Checking Software, Model Checking Techniques, Software Engineering