Correct composition in the presence of behavioural conflicts and dephasing
Correct composition in the presence of behavioural conflicts and dephasing
复制标题
DOI：
10.1016/j.scico.2019.102323
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
J. Bowles;M. Caminati
中科院分区：
文献类型：
--
作者：
J. Bowles;M. Caminati
执行场景通常用于指定系统中不同对象和组件之间的部分行为和交互。为了避免规范中的整体不一致，文献中出现了各种自动化方法来构建基于场景的模型。在最近的工作中，我们展示了如何将定理证明器 Isabelle/HOL 与 SMT 求解器结合起来，以检测序列图之间的不一致，并且仅在它们不存在的情况下生成行为组合。在本文中，我们进一步利用这种组合，并提出一种有效的方法，可以生成所有有效的组合轨迹，为我们提供无冲突有效组合模型的等效表示。此外，我们展示了一种新颖的方法来证明计算结果的正确性，并将该方法与仅在 Isabelle 内部完成的实现和验证进行比较。为了降低我们技术的复杂性，我们考虑优先级约束和分阶段模型的概念，即在不同时间开始执行的模型。这项工作的灵感来自于医学领域的一个问题，即不同的慢性病临床指南可能在不同的时间点应用于同一患者。我们通过该领域的实际示例来说明该方法。
Scenarios of execution are commonly used to specify partial behaviour and interactions between different objects and components in a system. To avoid overall inconsistency in specifications, various automated methods have emerged in the literature to compose scenario-based models. In recent work, we have shown how the theorem prover Isabelle/HOL can be combined with an SMT solver to detect inconsistencies between sequence diagrams and, only in their absence, generate the behavioural composition. In this paper, we exploit this combination further and present an efficient approach that generates all valid composed traces giving us an equivalent representation of the conflict-free valid composed model. In addition, we show a novel way to prove the correctness of the computed results, and compare this method with the implementation and verification done within Isabelle alone. To reduce the complexity of our technique, we consider priority constraints and a notion of dephased models, i.e., models which start execution at different times. This work has been inspired by a problem from a medical domain where different clinical guidelines for chronic conditions may be applied to the same patient at different points in time. We illustrate the approach with a realistic example from this domain.