Towards a Pattern-based Automatic Generation of Logical Specifications for Software Models

TL;DR

This paper proposes a method to automatically generate logical specifications from software models structured with predefined workflow patterns, facilitating deductive reasoning for correctness verification.

Contribution

It introduces a novel approach to transform workflow patterns into logical specifications automatically, addressing the challenge of obtaining complete logical specs for verification.

Findings

Enables automatic extraction of logical specifications from structured models.

Bridges the gap between deductive reasoning benefits and specification generation.

Facilitates correctness verification of software models.

Abstract

The work relates to the automatic generation of logical specifications, considered as sets of temporal logic formulas, extracted directly from developed software models. The extraction process is based on the assumption that the whole developed model is structured using only predefined workflow patterns. A method of automatic transformation of workflow patterns to logical specifications is proposed. Applying the presented concepts enables bridging the gap between the benefits of deductive reasoning for the correctness verification process and the difficulties in obtaining complete logical specifications for this process.