论文部分内容阅读
在涉及航空航天、交通指挥、军事、核工业等一些关键领域，系统一次计算的正确性，不单单取决于其计算逻辑的正确性，同时也与运行结果的产生时间、持续时间等有很大的关系。这样的系统，被称作为实时系统。实时系统关系国计民生，保证其设计和运行的正确性和可靠性至关重要。模型检测作为对实时系统进行形式验证的重要技术，在20世纪90年代获得繁荣的发展，并日益得到学术界的重视。模型检测算法的基本思路为将实时系统形式化抽象为其对应的模型，在模型的状态空间中，通过深度优先或广度优先的方式，搜索不满足特定性质规范的路径或者状态，若该路径或状态存在，则说明这个实时系统需要修改以提高其可靠性。CTAV是国际上第一个可针对时间自动机，使用线性时序逻辑刻画的性质规范进行验证的符号化模型检测工具，其检测范围局限于封闭的实时系统。 通常来说，实时系统的运行状态不仅仅取决于系统自身的运行结果，外界环境因素往往也直接或间接地影响着系统的整体运行状况。如果只考虑系统本身的状态迁移，很可能导致验证结果的不可靠，这就是控制器合成要解决的问题。它通过使用逻辑描述语言对系统要达成的目标进行描述，并利用时间博弈自动机对开放的实时系统进行建模，使用不同的算法在搜索模型状态的过程中验证是否有一个合成策略，使得系统无论环境因素如何作用，终能达到既定的目标。 为了弥补CTAV在开放实时系统验证这方面工作的空缺，本文将讨论在以时间博弈自动机为形式化模型的基础上，针对四种线性时序逻辑的基础性质所刻画的获胜目标，使用与之相对应的算法进行验证，其中以性质<>p，[]p，[]<>p为获胜目标的算法，Uppaal-Tiga在实现针对CTL性质的控制器合成算法中有涉及。作为LTL性质的构成要素，本文中同样实现了这些算法，在实现过程中，我们弥补了UppaM-Tiga的一些不足。此外，本文独创性地实现了<>[]p性质为获胜目标的合成算法，并利用符号化状态的包含关系对控制器合成算法加以优化，大大减少了内存的占用，从实验结果中可以看出，大约减少一个数量级。 最后，本文中设计和实现的控制器合成的工具CTAV/TGA，可以完成对大部分UPPAAL模型的解析和表示，并在其模型上完成四种获胜目标的验证。在本文中介绍算法时，通过对几个例子的分析，证明了验证结果的正确性。