UniversitÓ di Catania (ITALY)
CADP (Construction and Analysis of Distributed Processes)
Rapid evolution of both technology and markets leads to ever-increasing
complexity in business processes, particularly given the need to
respond quickly to changing market needs. It is therefore essential to
check the correctness of workflows, which represent abstractions of
business processes. This can be done using workflow management systems
(WFMS), but a formal, mathematical approach is rapid and more
effective. In particular, formal techniques based on process algebra
enable one both to provide a formal workflow specification and to
perform a verification of some desired properties.
The workflow design methodology is supported by workflow patterns, which represent the abstraction of activity sequences, and are composed when defining new workflows. Patterns are grouped into several classes: basic control flow (e.g., simple sequence, split, or join of activites); advanced control flow, where multiple active branches and synchronization are considered; structural patterns (e.g., loops); temporal and state-based patterns; and interworkflow synchronization patterns.
This work focuses on the formal specification of workflow patterns using the LOTOS formal description technique. Several kinds of patterns are considered: the AND-Split pattern, which models the concurrent execution of a set of activities running independently; the XOR-Split pattern, which selects a specific path based on control data and/or external decisions; the Milestone pattern, which describes the situation in which an activity is enabled just if a specified list of conditions (milestone) has been reached and not expired yet; and the Messaging communication pattern, which models the situation when information are exchanged between different activities, generally belonging to distinct workflows.
The usage of workflow pattern specifications in LOTOS is illustrated on a real case study, namely a workflow for the management of complaints, defined as a collection of activities and processes and the information that is exchanged between them. The workflow is specified in LOTOS using the AND-Split, XOR-Split, and Milestone patterns. The correctness of the resulting LOTOS specification, as well as some basic properties (absence of deadlock and livelock) were formally established using the CADP toolbox.
This case study demonstrates the value of applying formal description
techniques to workflow specifications. LOTOS is a suitable language for
specifying workflows, which can be done relatively easily, giving
access to verification tools such as CADP.
Vincenza Carchiolo, Alessandro Longheu, Michele Malgeri.
"Using LOTOS in Workflow Specification". Proceedings of the 5th
International Conference On Enterprise Information Systems, ICEIS 2003,
Available from our FTP site: PDF PostScript
Dipartimento di Informatica e Telecomunicazioni
FacoltÓ di Ingegneria
UniversitÓ di Catania
Viale Andrea Doria, 6
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|