失相行为模型的正确组合

执行场景通常用于指定系统中不同对象和组件之间的部分行为及交互。为避免规约中的整体不一致性，文献中已涌现出多种自动组合（行为）模型的方法。在近期工作中，我们展示了如何将定理证明器Isabelle与约束求解器Z3结合，以高效检测两个或多个行为模型中的不一致性，并在无冲突时生成其组合。本文进一步扩展了我们的方法，展示了如何为失相模型生成正确的组合（作为一组有效轨迹）。这项工作源于医学领域的一个问题：针对同一患者，不同的（慢性病）护理路径可能在不同的起始点被应用。