Formal and Model-Based Testing of Concurrent Workflows

The design of an information system will involve a number of structural and semantic integrity constraints. One way to ensure that these constraints are maintained is through the calculation and implementation of a guard for each operation: a condition sufficient for all integrity constraints to be maintained, checked before the operation is performed, if the guard evaluates false, then the operation will be blocked or rejected. The information required for the calculation of operation guards can be used also to calculate the effect of workflows: compositions or patterns of guarded operations. The multiplication of states and entities, for arbitrary, parallel compositions of operations and workflows, makes exhaustive analysis impractical. This paper shows how the precise specification of operations and workflows can be used instead to select particular scenarios for calculating effects at the model level, or for generating test cases at the implementation level. The result is an analysis and testing methodology for guarded workflows.