在安全攸关领域,如航空、航天、列车控制和医疗等,信息物理融合系统(Cyber-Physical System,CPS)具有很高的安全需求。在测试和仿真并不能保证没有系统错误的情况下,如何通过形式化建模与验证的方法保证系统安全是相关领域的重点关注问题。在动态实时的CPS系统中大量实时参数信息的存在会导致状态空间难以准确表示,从而使得传统的静态模型检验难以进行。针对此问题,相关学者提出了CPS系统在线建模与验证的方法,即利用参数信息在系统实际运转过程中不断更新且可获取这一特点,针对短时间周期内的系统行为建立模型并周期性验证。

然而,在对列车控制系统这个典型的CPS系统的分析过程中,本文指出在实际的CPS系统上应用在线验证存在两方面的问题。一方面,传统的流水线式的设计会存在的验证不能完全覆盖系统行为的问题,同时传统的设计中并没有考虑验证的时效性问题；另一方面,实际的列车车载设备计算能力有限,在线验证面临多车多任务等因素带来的效率问题。为了解决以上两个问题,确保在线验证的可靠性和高效性,本文的主要工作如下：1.提出了一种多机制触发下面向全周期覆盖的在线验证方法。以列控系统为例分析了流水线式在线验证过程中存在的覆盖问题和时效性问题,对在线验证设计过程中的几个重要参数进行了讨论,提出了一系列在线验证设计应满足的参数规约,在对验证规约进行了理论分析后,给出了在参数规约的指导下设计的多机制触发下面向全周期覆盖的设计方法,针对所提出方法我们设计了三组场景实验,从场景分析的角度说明了方法的必要性和正确性。2.提出了一种分布式的在线验证设计框架。通过对Linux Virtual Server技术思想的分析,从伸缩性、可靠性和透明性的角度出发,结合在线验证本身的特点,设计了一种在线验证的分布式框架,该框架包含任务配置模块,负载调度模块,后台验证模块和共享存储区。

在我们提出的框架设计的基础上搭建了进行了分布式在线验证云平台,并在云平台上进行了效率实验。3.与北京交通大学合作,在其轨道交通运行控制系统国家工程研究中心的北京亦庄线CBTC仿真测试子平台上进行了在线验证模块的设计与部署。通过对平台上亦庄线列车控制机制的分析建立了形式化模型,统一了车载设备接口信息并对实时参数进行了区段换算、曲线计算等一系列处理,对验证工具SpaceEx进行包装使其成为周期型验证后台,将在线验证模块部署在仿真平台的控制台上后设计了场景实验,证明了在线验证在实际的CPS系统上的有效性。