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.
|Title of host publication||On-line Proceedings 4th International SPIN Workshop (SPIN'98, Paris, France, November 2, 1998)|
|Editors||G. Holzmann, E. Najm, A. Serhrouchni|
|Publication status||Published - 1998|
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)