Verifying business processes using spin

W. Janssen, R. Mateescu, S. Mauw, J. Springintveld

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)


We present an application of the Spin model-checker in Testbed, a framework for business process reengineering. Business processes are described by end-users of Testbed in a graphi- cal language with a causality-based semantics, called Amber. The Amber language contains various constructs describing actions, causality relations, disabling, interaction and hierarchi- cal composition. Data entities are modelled as variables that are handled by the business processes. We present a validation methodology for business processes using model-checking techniques. In this approach, an Amber specification is automatically translated into a state machine description in Promela, which is the input language of the Spin model-checker. The correctness properties, concerning both the behavioural aspects and the data entities used in the specification, are checked on the resulting Promela program using Spin. A prototype verification toolset has been developed and successfully applied to various examples inspired from industrial Amber specifications.
Original languageEnglish
Title of host publicationOn-line Proceedings 4th International SPIN Workshop (SPIN'98, Paris, France, November 2, 1998)
EditorsG. Holzmann, E. Najm, A. Serhrouchni
Publication statusPublished - 1998

Fingerprint Dive into the research topics of 'Verifying business processes using spin'. Together they form a unique fingerprint.

  • Cite this

    Janssen, W., Mateescu, R., Mauw, S., & Springintveld, J. (1998). Verifying business processes using spin. In G. Holzmann, E. Najm, & A. Serhrouchni (Eds.), On-line Proceedings 4th International SPIN Workshop (SPIN'98, Paris, France, November 2, 1998)