面向修复具有丰富事件的基于场景的模型

修复遗留系统是一项困难且易出错的任务：通常，对这些系统复杂细节的有限了解可能使一次尝试的修复导致新的错误。因此，期望以自动化且可靠的方式修复此类系统。在此，我们讨论正在进行的关于基于场景的模型自动化修复工作：这类完全可执行的模型使用场景对象对其个体行为进行建模来描述系统。我们展示了如何对丰富的基于场景的模型进行模型检验，然后对其进行修复以防止各种安全违规。实际修复通过向模型添加新的场景对象而不改动现有对象来完成——这种方式与基于场景建模的原则高度一致。为实现修复方法的自动化，我们借助现成的SMT求解器。我们描述了该方法的主要原理，并讨论了未来的工作计划。