基于变化的、基于查询的运行时监控时序属性的基础

《Formal Aspects of Computing》：Foundations for Change-driven Query-based Runtime Monitoring of Temporal Properties

针对模型驱动工程中时间性和不完整痕迹的监控问题，提出确定语义（仅返回不受未来影响的答案）及改进的平淡语义（保持增量计算），分析其计算特性，并通过案例研究验证性能优于现有方法。

　　

摘要

在模型驱动工程中，通常通过基于查询的运行时监控来监视具有复杂动态结构的系统行为：运行时模型捕获系统状态的基于图的快照，而感兴趣的属性则通过图查询来表示，并在线对模型进行评估。对于时间属性，具有时间戳记录的快照跟踪被编码到运行时模型中，这些快照通过时间图查询来进行监控。在这种情况下，查询评估需要考虑到跟踪可能是不完整的，因此模型未来的变化可能会影响当前的查询结果。

在本文中，我们首次对基于查询的运行时监控进行了全面的形式化处理，该监控用于处理编码了不完整跟踪的时间属性。首先，我们为之前提出的一种查询方法引入了查询评估语义：之前的（普通）语义没有考虑不完整的跟踪，因此可能会返回可能受到模型未来变化影响的答案；而新的（确定性）语义只有在答案确定的情况下才会返回结果，即模型的未来变化不会影响这些答案。接着，我们为这两种语义提出了一种时间查询操作化的形式化方法，该方法支持增量式和基于变化的查询评估。然而，与普通语义不同，确定性语义依赖于模型的时间戳，因此必须重新计算跟踪中每个模型的所有答案；因此，确定性语义无法实现基于变化的评估。最后，我们提出了一种普通语义的变体，该变体能够在返回确定答案的同时保持基于变化的评估方式。我们通过两个案例研究评估了所提出语义的性能，并将其与现有技术进行了比较。