CTCS-3级列控系统车地交互流程形式化建模与验证

正在建设的时速300 km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程:任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心(RBC)、车载设备(ATP)和铁路专用移动通信网(GSM-R)的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.

一种嵌套中断系统的建模和分析方法

在嵌入式系统和各类操作系统中,中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中,往往会有更紧迫的中断事件请求响应,因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先,提出基于投影时序逻辑(projection temporal logic,简称PTL)的定义,并将这种定义推广到包含任意多中断事件的中断系统上,从而得出嵌套中断系统基于投影时序逻辑的形式化模型;其次,使用投影时序逻辑定义的基本中断语句扩充建模仿真和验证语言(modeling,simulation and verification language,简称MSVL),并扩展MSVL语言的解释器,使其可以对嵌套中断系统进行建模仿真和验证;最后,通过一个实例展现所提出方法的正确性和实用性.

基于单工架构的信息物理系统运行时安全性保障方法

运行时安全性保障方法旨在系统运行过程中确保安全性属性得到满足.基于单工(simplex)架构的运行时安全性保障方法能够在使用复杂且安全性未经验证的控制器的情况下,为系统提供安全性保证.其基本思想是将复杂且安全性未经验证的复杂控制器与经过严格形式化验证的安全控制器相结合,前者工作在无安全风险的情况下,若检测发现系统存在潜在的安全风险,则通过决策模块完成复杂控制器与安全控制器之间的切换,从而确保系统的安全性.本文重点关注基于simplex架构的信息物理系统运行时安全性保障方法,从simplex架构决策模块的设计、改进与拓展,以及simplex架构的应用3个方面展开研究,对相关工作进行了梳理和总结,指出当前面临的技术挑战,并展望未来的发展方向,认为基于simplex架构的运行时安全性保障方法将会是解决智能信息物理系统安全性保障问题的有效途径之一.

软件运行时验证与监控技术发展现状与展望

当今社会,大量软件系统运行在开放、动态、不确定的场景中,经常受到非预期的干扰和影响,因此对系统行为进行运行时验证与监控,并针对各种实时情况做出自适应的实时响应、决策与动态调控,具有重要意义。文章从运行时验证、监控、增强及动态调控等方面对相关领域的国内外进展进行了回顾与展望,并从软件行为认知与理解、控制器生成、全生命期监控等角度对后续潜在方向进行探讨与建议。