Verifying business processes using spin

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