Automatic Generation of Logical Specifications for Behavioural Models

被引:0
作者
Klimek, Radoslaw [1 ]
Witek, Julia [1 ]
机构
[1] AGH Univ Krakow, Krakow, Poland
来源
PROCEEDINGS OF THE 2024 WORKSHOP ON REPLICATIONS AND NEGATIVE RESULTS, RENE 2024 | 2024年
关键词
generating logical specification; behavioural model; workflow mining; theorem prover;
D O I
10.1145/3695750.3695822
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:1 / 7
页数:7
相关论文
empty
未找到相关数据