This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05)
Proof Slicing with Application to Model Checking Web Services
Seattle, Washington
May 18-May 20
ISBN: 0-7695-2356-0
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.
Citation:
Purdue University, Wei-Tek Tsai, Raymond Paul, "Proof Slicing with Application to Model Checking Web Services," isorc, pp.292-299, Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.