Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05) (2005)
May 18, 2005 to May 20, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ISORC.2005.44
Purdue University , Arizona State University, Tempe, AZ
Wei-Tek Tsai , Arizona State University, Tempe, AZ
Raymond Paul , OSD NII, Department of Defense
Web Services emerge as a new paradigm for distributed computing. Model checking is an important verification method to ensure the trustworthiness of composite WS. Boolean 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 precision 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 existing abstraction-based model checking techniques, e.g., lazy abstraction. Besides the correctness and termination proofs, we also conducted theoretical analysis on the performance of the proof slicing algorithm.
P. University, R. Paul and W. Tsai, "Proof Slicing with Application to Model Checking Web Services," Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05)(ISORC), Seattle, Washington, 2005, pp. 292-299.