Mind the Gap: Addressing Behavioural Inconsistencies with Formal Methods
Mind the Gap: Addressing Behavioural Inconsistencies with Formal Methods
复制标题
DOI：
10.1109/apsec.2016.051
复制
发表时间：
2016-12
期刊：
影响因子：
--
通讯作者：
J. Bowles;M. Caminati
中科院分区：
文献类型：
--
作者：
J. Bowles;M. Caminati
在复杂的系统设计中，重要的是要构建几个设计模型，侧重于系统的不同方面，以更好地了解单个组件的结构和行为。执行场景通常用于指定一组系统对象或组件之间的部分行为和交互。然而，部分规范可能会隐藏不一致或其他无意中不完整或未充分指定的行为模型。本文提出了一种新的强大的技术相结合的约束求解器和定理证明，以完成部分规格，并确定整体模型的不一致性。我们使用一个真正的并发模型，即标记的事件结构，它可以被用作广泛使用的工作流或基于XML的语言的底层语义。我们展示了如何定理证明器Isabelle和约束求解器Z3之间的相互作用可以用于检测和解决部分规范和事件结构的不一致。
In complex system design, it is important to construct several design models focusing on different aspects of a system to gain a better understanding of individual component structure and behaviour. Scenarios of execution are commonly used to specify partial behaviour and interactions between a group of system objects or components. However, partial specifications may hide inconsistencies or an otherwise unintentionally incomplete or underspecified behavioural model. This paper proposes a new powerful technique combining constraint solvers and theorem provers to complete partial specifications and determine overall model inconsistencies. We use a true-concurrent model, namely labelled event structures, which can be used as the underlying semantics of widely used workflow or scenario-based languages. We show how an interplay between the theorem prover Isabelle and constraint solver Z3 can be used for detecting and solving partial specifications and inconsistencies over event structures.