定时自动机轨迹中的不可行的识别的有效源

摘要

本发明涉及定时自动机轨迹中的不可行的识别的有效源。具体地，公开了一种用于验证被建模为定时自动机的实时系统性能的方法。系统的抽象模型依据初始线性时序逻辑规格被检查。如果发现通向不希望状态的路径，反例使用负循环检测被验证或使其无效。如果检测到负循环，进行优化来识别负循环中的最小不可行片段。然后规格被细化以消除最小不可行片段的使用，然后抽象模型依据被细化的规格被检查。

主权项

一种用于在定时自动机轨迹中识别最小不可行片段的方法，所述方法可在数字计算机上编码的算法中应用，所述方法包括：提供反例，其中所述反例是到不希望状态的路径，所述不希望状态是通过依据时序逻辑规格来检查定时自动机的抽象模型而被识别的；使用负循环检测验证所述反例或使所述反例无效；如果检测到负循环，在所述反例中识别不可行片段；以及优化所述不可行片段以产生最小不可行片段，其中，优化所述不可行片段包括结合和缩小不等式以产生最小不可行片段，其包括最小数量的位置、轨迹线和分量。