Workflow Specification using LOTOS

Organisation:	Università di Catania (ITALY)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Business processes.
Period:	2003
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Carchiolo-Longheu-Malgeri-03] Vincenza Carchiolo, Alessandro Longheu, Michele Malgeri. "Using LOTOS in Workflow Specification". Proceedings of the 5th International Conference On Enterprise Information Systems, ICEIS 2003, April 2003. Available from the CADP Web site: PDF PostScript
Contact:	Vincenza Carchiolo Dipartimento di Informatica e Telecomunicazioni Facoltà di Ingegneria Università di Catania Viale Andrea Doria, 6 I95125 Catania Italy Phone: +39-095-738-2359 E-mail: Vincenza.Carchiolo@diit.unict.it
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page