A Petri Net-Based Specification Model Towards Verifiable Service Computing

Abstract

The emerging paradigm of Web services opens a new way of engineering enterprise Web applications via rapidly developing and deploying Web applications by composing independently published Web-service components to conduct new business transactions. However, how to formally validate and reason about the properties of an enterprise system composed of Web-service components remains a challenge. This chapter introduces an advanced topic of enterprise service computing: the formal verification and validation of enterprise Web services. The authors introduce a Web-services net (WS-Net), which is an executable architectural description language incorporating the semantics of colored petri nets with the style and understandability of the object-oriented concept and Web-services concept. As an architectural model that formalizes the architectural topology and behaviors of each Web-service component as well as the entire system, WS-Net facilitates the simulation, verification, and automated composition of Web services.