论文部分内容阅读
轨道交通这样的实时系统对时间的要求及其严格，要保障轨道交通运营场景的安全性，就需要对运营场景进行安全检测，而保证系统安全性的关键任务就是实时系统的时间约束的满足性。针对此问题，模型检测技术得以应用，模型检测的原理是为系统建立模型，用时态逻辑表示需要检测的性质，然后用检测算法检测该模型是否满足性质。使用的检测工具是UPPAAL工具，根据检测步骤需要理解UPPAAL工具的模型时间自动机的构造及如何用规范语言表示性质，还要理解其检测算法的实现。本文针对轨道交通的运营场景之一的RBC切换场景进行验证，使用UPPAAL工具验证其切换过程中的安全性。 对实时系统的绝大多数安全性和活性的检测，模型检测都是通过可达性分析算法来完成。可达性分析算法是模型检测的基础，由于时间自动机的时间约束而加速了状态空间爆炸，增加了可达性分析算法的复杂性。已存的时间自动机可达性分析算法，或是基于等价时间区域图(Region)、有界差分矩阵(DBM)采用半符号时间约束结构的状态空间遍历分析方法;或是基于BDD结构采用全符号时间约束的状态空间遍历方法。这两类方法割裂了状态变迁表达与时间约束表达符号关联，难以应用大规模案例分析。本文的主要工作是: 1)采用常用的检测工具是UPPAAL工具，对典型的轨道交通运营场景进行功能安全性和时间约束的安全性进行检测，从而能够实现系统模型的安全性分析。 2)提出一种全符号的可达性分析方法，采用BDD结构统一表达时间自动机的状态变迁空间和时间约束，给出了在状态可达全符号运算的基础上时间约束的运算系列算法，并给出了单自动机、多自动机的可达算法。 最后实例验证算法的正确性。通过这种方法，可以实现时间自动机的全符号化可达性分析，为全符号时间系统模型检测提供分析基础。