基于车车通信的列控系统是下一代列控系统的典型代表。该系统引入车车通信技术,采用移动闭塞技术行车,以卫星定位方式代替轨道电路实现列车自主定位与完整性检测,由车载设备计算行车许可并实现进路排列。由于该列控系统正处于理论探索和方案设计阶段,对系统特定场景进行安全分析和形式化验证,识别不安全行为及行为致因并以此制定安全性设计需求是十分必要的,可以在系统设计初期避免危险事件的发生。论文以基于车车通信的列控系统为研究对象,构建其多分辨率STAMP模型,采用改进后的STPA安全分析方法对系统的特定场景进行安全性分析,得到了引起危险事故的诸多致因;根据危险致因定义了安全性设计需求,并对其进行了验证。论文完成的主要工作有:(1)提出了一种针对基于车车通信列控系统的安全分析方法。首先,根据该系统的结构和特点,从不同层面关注列控系统的控制和反馈过程,对传统STAMP模型进行改进,构建了列控系统的多分辨率STAMP模型,旨在解决单一STAMP模型无法对列控系统复杂场景进行全面描述,进而导致安全分析不充分的问题。然后,鉴于传统STPA方法无法区分危险致因是否是导致事故发生的根本原因,在该方法中定义了描述多分辨率STAMP模型的行为关系BR(Behavior Relation),用于描述当前STAMP模型内部各组件间不安全行为发生的原始与非原始致因。在此基础上,沿着分辨率等级和行为关联路径对各级STAMP模型进行迭代安全性分析,直至获得所有引起危险事件的原始致因。最后,根据原始致因提出安全性设计需求(Safety Design Requirements,SDRs)。(2)选取典型运营场景,对基于车车通信的列控系统进行了安全性分析。以列车出车辆段至区间追踪运行场景为例,主要包括列车自主定位、前车识别、车车通信及车载自主计算行车许可等过程。结合该场景下车载设备(OBE)子系统、动态运能决策(DCD)子系统及资源管理单元(RMU)子系统的内部结构和外部信息交互流程,划分分辨率等级并构建相应的UML静态与动态模型。通过本文提出的UML向多分辨率STAMP模型的转换规则,建立相应的多分辨率STAMP模型。在此基础上,根据分辨率等级从低到高逐层分析,直至得到所有引起系统危险的原始致因,并根据危险致因提出了待分析场景下的SDRs。(3)对基于车车通信的列控系统是否满足安全性设计需求进行了验证。将安全性设计需求转换为UPPAAL能够验证的BNF语句,并将其分为功能性、时序性及安全性三类。在待分析场景下,针对低分辨率层面的车载设备及其交互设备建立时间自动机模型,并整合成时间自动机网络,对BNF语句进行验证。验证结果表明,目前基于车车通信的列控系统满足车载设备子系统低分辨率STAMP模型分析得到的安全性设计需求。本文共有图58幅,表39个,参考文献71篇。