摘要

In open and changeful Internet, the enterprise business process needs to be organized or restructured dynamically in order to adapt to environment changes and business logic updates. The solution of Web service and service-oriented architecture (SOA) provides a promising approach. The business processes working as a temporary workflow can be composed by distributed services. However, the cross-organizational service feature of business process requires considering not only the functional requirements but also the timed constraints. The timed property plays an important role in service interactions between business processes, such as timed activity, timeout and timed deadlock. Thus, if time requirements cannot be guaranteed, the new created business process will not be acceptable. In this paper, it proposes a framework of using Petri Net to model timed service business process. First, it deflnes the behavior model of service business process and gives process composition patterns for different structural forms. Second, service model is extended with time speciflcations, describing timed constraints among business activity interactions. Third, to support further veriflcations, it introduces a method for the automatic timed properties generation in the form of temporal logic formulae. Our framework gives a reference in practice to formalize service business process into timed service model.