It has been argued that Event Calculus (EC) is suitable for modeling high-level specifications of safety-critical cyber-physical systems. The primary advantage lies in the rather small semantic gap between EC models and requirements expressed in a semi-formal natural language. Moreover, its use of continuous time and variables avoids imprecision that stems from discretization. In the past, we have shown that a goal-directed ASP system can be used for implementing these EC models. However, precise representation of time as an infinitesimally divisible continuous quantity leads to Zeno-like behaviors and to non-termination in such a system. In this work, we model a number of well-known example problems from the literature to systematically study various natural EC modeling patterns that yield these Zeno-like behaviors, and propose ways to deal with them. Moreover, we also propose a technique to automatically detect all such cases.
翻译:已有观点认为,事件演算(EC)适用于对安全攸关的信息物理系统进行高层规范建模。其主要优势在于EC模型与用半形式化自然语言表达的需求之间的语义鸿沟较小。此外,其对连续时间和变量的使用避免了因离散化而产生的精度损失。过去我们已证明,目标导向的ASP系统可用于实现这些EC模型。然而,将时间精确表示为无限可分的连续量会导致此类系统中出现芝诺式行为及非终止现象。本研究通过建模文献中多个经典示例问题,系统性地考察了导致这些芝诺式行为的多种自然EC建模模式,并提出了相应的处理方案。此外,我们还提出了一种可自动检测所有此类情况的技术。