谓词抽象验证密集实时系统安全性与复杂性

本文主要探讨了"密集实时系统的谓词抽象及其验证方法"。该研究聚焦于在实时系统领域，尤其是在处理安全性与复杂性方面的一种创新技术——谓词抽象。谓词抽象作为一种工具，被用来确保这些系统在满足严格的实时约束的同时，能够有效地验证其关键属性，如安全性和活性。 首先，作者定义了一种时间系统的限制语义，这种新定义的语义在观察层面上与标准语义保持等价，因为它们能够验证同样的演算公式，而且无需依赖后续操作符。这种限制语义的引入简化了验证过程，使得分析更加精确。 接下来，研究将传统的模型检测问题——即确定一个时间自动机（TA）S和一个演算公式之间的关系——转换为对TA的谓词抽象。当一组抽象谓词构成所谓的基础时，形成的抽象能够确保在S中验证某个有限抽象公式，即所谓的“强保留”。这样，验证过程就可以通过已有的模型检查技术来实现，尽管这通常涉及复杂的算法，如时间自动机的区域图构造。 然而，由于计算成本，研究人员指出，仅依赖基础的抽象谓词集合可能不总是最优解。他们提出了一个迭代的方法，从粗糙的抽象开始，逐步构建一个有限的抽象序列，最终达到强保留的抽象。这个过程中，如果模型检查尝试失败，会作为启发式策略引导选择新的抽象谓词，以优化抽象的精度。 值得一提的是，这项研究得到了美国国家科学基金会的多个项目资助，以及NASA兰利研究中心与霍尼韦尔公司的合同支持，部分研究工作是在2001年7月/8月期间在SRI国际进行的。此外，还与德国乌尔姆大学进行了合作，并且论文在2002年由Elsevier Science B以开放访问的形式发布，遵循V.CCBY-NC-ND许可。 这篇文章提供了一种创新的工具和技术，旨在提高密集实时系统验证的效率和有效性，特别是在处理复杂实时约束和确保系统性能的同时，确保其符合预定的安全和功能性需求。通过谓词抽象的运用，研究人员不仅简化了验证流程，也为实际应用中的实时系统设计和验证带来了新的可能性。