高速铁路列控系统安全性验证的一阶可判定形式理论研究

高速铁路列车运行控制系统的安全性至关重要。形式化技术是验证系统行为属性的有效手段之一。但目前的形式化技术，或者不能准确刻画列控系统安全功能行为的演化特征，或者描述列控系统的安全功能行为特征后没有可判定的算法，导致难以对列控系统安全性开展完备形式化验证。本课题选取一阶逻辑中存在的可判定子集，研究其可判定保持的扩展和组合方法，形成基调，用代数状态等价方法建立统一的语义框架，将UML描述的场景转化为一阶形式语言描述的公理集，利用一阶逻辑自身的推导规则，最终构建可判定一阶形式理论。形式理论的形成过程中，通过公理集的无矛盾性证明来保证公理集存在解释模型，使用启发式的可满足性判断算法，结合可判断子集判定过程的有机组合实现高效判定过程。该形式理论可精确刻画复杂场景下高速列车控制系统的行为及安全功能属性的演变规律，并实践于其安全性验证，对相关安全苛求领域的系统安全性验证具有指导作用。

高速铁路列车控制系统的安全性至关重要，形式化技术是验证列车控制系统安全性的重要手段。本课题以列车控制系统的安全功能行为演化特征为基础，选择时间自动机和线性混成自动机作为列车控制系统形式化建模语言，通过构建自动机网络刻画列车控制系统的行为演化和不同部件之间的行为交互。为了实现对列车控制系统的有效验证，课题组分别采用一阶逻辑中可判断的微分和线性算术理论对时间自动机和线性混成自动机构成的网络进行编码，提出一种更有效的复合离散和连续变迁的实时系统编码方案。由于时间和线性混成自动机是一类能够描述系统行为随时间连续变化的形式化描述语言，基于符号化编码的有界模型检测不存在完备性上界。因此，课题组结合一阶逻辑的插值定理和有界模型检测技术，实现了对时间自动机等形式模型的安全性等性质的验证。此外，为了确保列车控制系统交互过程与消息序列图描述的运行场景规范一致，本课题将消息序列图转化为一阶约束公式，并结合表示列车控制系统的时间自动机网络进行归纳证明，从而实现对场景的不可行性等性质的证明。最后，在本报告中课题组给出了列车控制系统中的车站联锁子系统的验证过程作为案例说明基于可判定形式理论的验证技术的有效性。