基于微分逻辑的轨道交通运营实时场景全符号化模型检测技术研究

项目名称： 基于微分逻辑的轨道交通运营实时场景全符号化模型检测技术研究

项目编号： No.61273180

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 杜军威

作者单位： 青岛科技大学

项目金额： 84万元

中文摘要： 交互控制执行的时效性是影响分布式列车控制系统安全性的重要因素。形式化技术是验证系统行为属性的有效手段。但目前形式化技术或采用基于可达性模型检测方法无法验证具有无限状态空间的时间自动机组合模型；或采用符号化模型检测方法无法获得通用的兼顾符号表示紧致性和执行效率的方法，从而难以形成可实用的轨道交通运营实时场景验证方法。本项目针对轨道交通运营场景特征，提出基于微分逻辑的全符号化模型检测算法：采用基于局部时钟语义偏序约简方法，降低组合过程中路径集空间爆炸问题；采用基于假设保障的复杂部件替换方法，降低复杂部件组合过程中的状态空间爆炸问题，获得可兼顾符号表示紧致性和执行效率、适用于轨道交通运营实时场景可行的形式化验证方法。该形式理论为复杂问题的逼近求解提供了系统性的构造方法和有效算法，可验证复杂实时场景下实时交互行为及随时间演变行为的安全性，对相关安全苛求领域的系统安全性验证具有指导作用。

中文关键词： 铁路信号系统；软件安全性需求；模型检测；安全性验证；安全性测试

英文摘要： The execution timeliness of interactive control instruction is an important safety factor of distributed train control system. Formal technology is an effective means to verify the properties of the system behavior. But there are two types of problems in the formal technique currently used to validate operational real-time scenario models. First, the combination of timed automata model with infinite state space cannot be verified by reachability model checking technique. Second, the compactness and efficiency in the implementation of symbolic model checking methods are difficult to take into account. Thus it is difficult to obtain a practical verified method about the safety of rail transport operational real-time scenario. According to the characteristics of the rail transport operational real-time scenario, we propose a fully symbolic model checking algorithm based on differential logic. Using partial order reduction method based on local clock semantic, space explosion problem can be achieved effective mitigation by reducing the size of path set in the composition process of time automata. Using the complex components replacement methods based on Assumption/guarantee technique, space explosion problem can be achieved effective mitigation by reducing state space of complex components in the composition proces

英文关键词： Railway Signal System；Software Safety Requirement；model checking；safety verification；safety testing