Proof slicing with application to model checking Web services

Hai Huang, Wei Tek Tsai, Raymond Paul

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, ISORC 2005
Pages292-299
Number of pages8
DOIs
StatePublished - 2005
EventEighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, ISORC 2005 - Seattle, MA, United States
Duration: May 18 2005May 20 2005

Publication series

NameProceedings - Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, ISORC 2005
Volume2005

Other

OtherEighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, ISORC 2005
CountryUnited States
CitySeattle, MA
Period5/18/055/20/05

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Proof slicing with application to model checking Web services'. Together they form a unique fingerprint.

Cite this