Automatic Generation of Logical Specifications for Behavioural Models

Logical specifications for behavioural models are crucial for the formal analysis of complex system designs. The automation of obtaining such a specification is essential particularly for promoting logical and deductive methods in software development. This article replicates earlier methods for aut...

Full description

Saved in:
Bibliographic Details
Main Authors: Klimek, Radoslaw, Witek, Julia
Format: Conference Proceeding
Language:English
Subjects:
Analytical models
Automation
behavioural model
Complex systems
Computational modeling
Conferences
Data mining
generating logical specification
Information systems
Information systems > Information systems applications
Logic
Software development management
Software engineering
theorem prover
Theory of computation > Logic > Logic and verification
workflow mining
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Logical specifications for behavioural models are crucial for the formal analysis of complex system designs. The automation of obtaining such a specification is essential particularly for promoting logical and deductive methods in software development. This article replicates earlier methods for automatically generating logical specifications equivalent to behavioural models, while also extending the approach to include workflow mining processes. Various and effective interactions with existing theorem provers are also proposed. We conducted straightforward, yet comprehensive, experiments covering multiple stages, which include workflow extraction, automatic logical specification generation, and theorem prover based analysis and the evaluation of these specifications.
ISSN:2151-0849
DOI:10.1145/3691621.3694927