A system for deduction-based formal verification of workflow-oriented software models

DOI10.2478/AMCS-2014-0069zbMATH Open1309.68131arXiv1402.1978OpenAlexW3123419187MaRDI QIDQ2018423FDOQ2018423

Authors: Radosław Klimek 

Publication date: 14 April 2015

Published in: International Journal of Applied Mathematics and Computer Science (Search for Journal in Brave)

Abstract: The work concerns formal verification of workflow-oriented software models using deductive approach. The formal correctness of a model's behaviour is considered. Manually building logical specifications, which are considered as a set of temporal logic formulas, seems to be the significant obstacle for an inexperienced user when applying the deductive approach. A system, and its architecture, for the deduction-based verification of workflow-oriented models is proposed. The process of inference is based on the semantic tableaux method which has some advantages when compared to traditional deduction strategies. The algorithm for an automatic generation of logical specifications is proposed. The generation procedure is based on the predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea for 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 intuitiveness of the deductive reasoning and the difficulty of its practical application in the case when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing our understanding of, the deduction-based formal verification of workflow-oriented models.

Full work available at URL: https://arxiv.org/abs/1402.1978

Recommendations

• Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models
• A Graph Transformation-Based Approach to Formal Modeling and Verification of Workflows
• A formal verification technique for behavioural model-to-model transformations
• WorkflowFM: a logic-based framework for formal process specification and composition
• KeY: A Formal Method for Object-Oriented Systems

zbMATH Keywords

temporal logicsemantic tableauxformal verificationdeductive reasoningbusiness modelsworkflow patternsBPMNgenerating logical specificationslogical primitives

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated deduction for verification
• Title not available (Why is that?)
• Defining liveness
• Title not available (Why is that?)
• Property specifications for workflow modelling
• Temporal and dynamic logic

Cited In (6)

• WorkflowFM: a logic-based framework for formal process specification and composition
• Title not available (Why is that?)
• Theorem prover approach to semistructured data design
• The formal derivation of algorithm and automatic verification based on Isabelle
• Constraint Solving for Verifying Modal Specifications of Workflow Nets with Data
• Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models

Uses Software

• YAWL
• CalcCheck

This page was built for publication: A system for deduction-based formal verification of workflow-oriented software models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2018423)