Title page for ETD etd-08092006-005135

Type of Document

Dissertation

Author

Cheng, Zhengang ,

Author's Email Address

zcheng@eos.ncsu.edu

URN

etd-08092006-005135

Title

Verifying Commitment Based Business Protocols and their Compositions: Model Checking using Promela and Spin

Degree

PhD

Graduate Program

Computer Science

Advisory Committee

Advisor Name	Title
Mladen A. Vouk	Committee Co-Chair
Munindar P. Singh	Committee Co-Chair
Laurie Williams	Committee Member
Peter R. Wurman	Committee Member

Keywords

verification
model checking
SPIN
OWL
protocol composition
service composition
web services

Date of Defense

2006-08-10

Availability

unrestricted

Abstract

A protocol-oriented approach of modeling and enacting
business processes and workflows has been developed recently that offers
advantages in terms of supporting the autonomy and heterogeneity of
business partners and the reconfigurability of their process.
Importantly, protocols are described using commitments, map to the
individual computation of the participating roles, and can be composed
to yield more complex protocols. However, verifying that the protocols,
especially composed protocols, fully satisfy appropriate correctness
properties remains an open problem.

This dissertation presents a novel way to model business protocols in
terms of commitments involved and the constraints for protocol
composition. The correct composition of a business process can be expressed via
individual protocol definitions and their composition constraints,
thereby enabling the verification of large processes.
Importantly, as part of the verification process,
protocols are translated into the language Promela, which makes them
amenable to analysis and verification using the model checker Spin. As a
result many important properties of business protocols and their
compositions into partial and full workflows can be verified, and
improved protocols can be produced.

The contribution of this dissertation is in providing a generalized mechanism for modeling
commitments, formulating and verifying properties related to
commitments. In fact, the results are applicable to a wide range of
processes and related protocols, such as scientific discovery processes
and workflows.

Files

Filename		Size	Approximate Download Time (Hours:Minutes:Seconds)
Filename		Size	28.8 Modem	56K Modem	ISDN (64 Kb)	ISDN (128 Kb)	Higher-speed Access
	etd.pdf	452.08 Kb	00:02:05	00:01:04	00:00:56	00:00:28	00:00:02