Database of Case Studies Achieved Using CADP

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 our FTP site: PDF PostScript

Vincenza Carchiolo
Dipartimento di Informatica e Telecomunicazioni
FacoltÓ di Ingegneria
UniversitÓ di Catania
Viale Andrea Doria, 6
I95125 Catania
Phone: +39-095-738-2359

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page