online read us now
Paper details
Number 4 - December 2014
Volume 24 - 2014
A system for deduction-based formal verification of workflow-oriented software models
Radosław Klimek
Abstract
The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal
correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of
temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach.
A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The
process inference is based on the semantic tableaux method, which has some advantages when compared with traditional
deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure
is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of
business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a
kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical
specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive
reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has
gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of
workflow-oriented models.
Keywords
formal verification, deductive reasoning, temporal logic, semantic tableaux, workflow patterns, logical primitives, generating logical specifications, business models, BPMN