PostScript
Verifying Business Processes Using SPIN
Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld
Proceedings of the 4th International SPIN Workshop (Paris, France),
November 1998.
Abstract:
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 graphical language with a causality-based semantics, called AMBER. The AMBER language contains various constructs describing actions, causality relations, disabling, interaction and hierarchical 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.
| 16 pages | |
PostScript |
| Slides of R. Mateescu's lecture at SPIN'98 | |