|
VERBUS (VERification for BUSiness processes)
is a modular and extensible
framework for automatic business process verification. It
proposes an architecture with three layers: the design
layer, the formal layer and the verification layer. The
formal layer is a business process specification model based
on FSMs formalism. It disconnects process description
languages and verification languages. Process definitions
(design layer) can be automatically translated to
specifications in the formal layer. These specifications can
be automatically translated to specifications in the
verification layer and verified using verification tools.
The current prototype of VERBUS uses BPEL4WS as process
definition language (design layer). It can generate
Promela and SMV verifiable models. Promela models can
be verified with Spin.
SMV models can be verified with
SMV
or NuSMV.
|
