基于STPA和时序逻辑的RBC切换场景安全分析_林经源.pdf

数据库系统设计Database System Design电子技术与软件工程Electronic Technology&Software Engineering210随着中国高铁技术的不断完善和升级，高铁在人民的出行中占据了越来越重要的地位，这也意味着一旦高铁行车过程中出现危险，会对人民的生命财产安全造成严重威胁。为满足我国铁路运输日益增长的运营需求，在保证安全的前提下，我国在列车控制系统领域博采众长，自主开发了 CTCS（Chinese Train Control System，中国列车控制系统）。其中我国现行高速铁路主要干线中使用的是 CTCS-3 级列控系统（下简称为 C3 系统）。为保证安全性、可靠性、可用性和稳定性等各方面性能，我国对 C3 系统有着严格的要求，以国际标准 IEC61508为标准，CTCS-3 级列控系统设计使用前需要经过严格的安全分析与测试工作，为了保证系统在均满足现行规范要求，进而保障人们生命和财产安全。现有大部分针对复杂系统的安全性分析中，故障树分析，故障模式及影响分等方法将系统的安全性问题拆分，由多个组件的可靠性来保证最终复杂系统的安全性。这些方法了较好的效果，但是这些方法难以针对复杂系统中的多个组件交互中可能出现的安全问题进行分析。系统理论过程分析将安全性问题转化为控制问题，能够针对多个组件间的相互作用中可能出现的安全性问题进行分析，在航空，医疗，交通，项目管理等领域的安全性分析中进行了广泛的应用，取得了一定的成就。根据现场实际运行情况来看，列控系统组件和功能复合度较强，现行分析中针对各个组件的分析已经不能较好的描述现场中出现的多组件之间的共同作用的复合故障，本文基于 STPA 分析，并且使用时序约简，提出一种寻找复合故障可能出现情况的方法，为实际现场测试提供参考。1 基本理论1.1 STPA原理系 统 理 论 的 过 程 分 析(System-Theoretic Process Analysis,STPA)由 Leveson 于 2003 年 提 出1。这 种方法基于系统理论事故建模和过程(Systems-Theoretic Accident Modeling and Processes，STAMP)，是一种近几年来发展迅速的新型安全分析方法。STAMP 采用分层控制结构来描述部件间的控制关系，如果这些控制能满足安全约束条件则系统是安全的。在 STAMP 理论中指定一下 4 种不恰当控制关系：（1）控制器没有提供本应提供的控制行为，或控制行为没有被很好地执行，可以用 N(Not Provided)来记基于 STPA 和时序逻辑的 RBC 切换场景安全分析林经源1*何涛2（1.兰州交通大学自动化与电气工程学院 甘肃省兰州市 730070）（2.兰州交通大学自动控制研究所 甘肃省兰州市 730070）摘要：本文提出一种利用时序逻辑运算的方法对系统理论的过程分析进行扩展的方法。首先建立对应的系统理论的事故模型及过程，参考列控系统的十四个运营场景进行细化，以 RBC 切换场景为例，进行系统安全性分析。最后结合时序逻辑约简来辨识可能出现的复杂系统危险。关键词：系统理论过程分析；时序约简；CTCS-3 级列车控制系统；RBC 切换基金项目：国家自然科学基金-铁路基础研究联合基金面向复杂环境的列车自主运行控制状态全息感知理论与关键技术研究（项目编号：U2268206）；2022 年度甘肃省重点人才项目面向铁路信号系统的数字孪生应用平台研究（项目编号：2022RCXM014）。图 1：STPA 的实施步骤数据库系统设计Database System Design电子技术与软件工程Electronic Technology&Software Engineering211录；（2）控制器错误提供了控制行为或提供了不安全的控制行为，记录为 I(Incorrect)；（3）控制行为出现在错误的时间，即过早(E,Early)或者过晚(L,Late)；（4）正确的控制行为停止的过早或持续过久，即持续时间(T,time)问题。STPA 旨在发现以上不恰当控制关系，并对其成因加以分析。其分析步骤如图 1 所示。STPA 可有效从控制的角度对系统的不恰当行为进行分析，但是列控系统作为多控制器的复杂控制系统，部件间有复杂的时序逻辑关系。考虑一个控制行为是否恰当还需针对其触发的时序逻辑进行分析，而 STPA 方法难以进行详细的时序逻辑描述。我们需要一种针对控制行为的时序逻辑情况进行分析的完成不恰当行为的辨识。1.2 基于时序逻辑的不恰当行为分析方法一般而言，控制命令本身是有时间的，STAMP 中第四条控制风险就是针对存在控制命令本身有较长持续时间的情况，但是在列控系统中，大部分控制命令下达是为一个具体时点。控制行为发生后就已经引起了系统的变化，本文再讨论时序逻辑描述时将控制行为发生的时点进行定位，讨论一个控制行为在对应时点上是否已经发生，故暂时不考虑控制行为持续时间的问题。本文使用逻辑是与非（）来表现控制命令情况是否与描述一致。因实际运行中时序逻辑关系较为复杂，故在此引入布尔逻辑符号且（）和或（）来描述两控制命令同时发生和两事件均独立发生。具体的参考时间点放在最后，用“|”隔开，表示该时间点前是否发生。则“列车依次实施常用制动（SB）和紧急制动（EB）”可以被描述为 SB|EB，即是在紧急制动发生时，常用制动已经发生。因德摩根律在经典命题逻辑的外延中依然有效，我们可以根据德摩根律归纳一系列的约简法则来约简实际情况中较为复杂的时序逻辑关系。其约简法则如下所示：(nAn|t)=n(An|t)（1）(nAn|t)=n(An|t)（2）这里针对式1-1给出证明：设x为t时间点前的时刻，则：xA1,xA2,xA3xA1,xA2,xA3xA1A2A3式 1-1 证毕。因实际时间节点选取更复杂和灵活，在这里补充两个时序表达式约简方法，以针对复杂时许情况下同一事件多次出现的情况：A|ntn=nA|tn （3）A|ntn=nA|tn （4）这里对式 1-3 给出证明：设 A 事件发生的时间为 T，则：Tfirstt1,t2,t3Tt1,Tt2,TsbireqEB:n|speedebi reqSB:l|speedsbireqEB:l|speedebi因行车速度超速的情况下，常用制动速度低于紧急制动速度，其时点也对应更早。所以在此式中 speedsbi的时点一定在 speedebi 之前，故可以将原式简化如下Speed:iVLocagtion:i=reqSB:n|speedsbireqEB:n|speedsbi reqSB:l|speedsbireqEB:l|speedsbi这里就可以应用先前的约简公式，将该式约简为：Speed:iVLocagtion:i=(reqSB:n reqEB:n)|speedsbi (reqSB:iVreqEB:i)|speedsbi在此例中，与 reqSB，reqEB 相关的部分均以化简结束，即在这个环节中，常规制动命令和紧急制动命令有关的危险情况均已分析完成，即超过限制速度时，紧急停车。命令均未提供或两命令均过晚，在此化简基础上，因常用制动一定在紧急制动发生之前，在这里可以在最后对常用制动与紧急制动之间这段约束进行约简，可以将其化简为：图 2：CTCS-3 级列控系统构成及接口图表 1：RBC 切换场景时序约简结果及含义时序约简式约简结果含义Emergency:n|Emergency Condition紧急情况时没有提供紧急停车命令Emergency:l|Emergency Condition紧急情况时过晚提供紧急停车命令MA:i|Emergency:e紧急制动前提供错误 MAMAshorten:I|Emergency:e紧急制动前过晚缩短行车许可reqSB:n|reqEB:n无常用及紧急制动命令reqSB:l|reqEB:l常用及紧急制动命令发生过晚RBClimit:i|COMM Built错误的临时限速信息RBClimit:n|COMM Built没有临时限速信息数据库系统设计Database System Design电子技术与软件工程Electronic Technology&Software Engineering213Speed:iVLocagtion:i=reqSB:n|reqEB:n reqSB:l|reqEB:l按以上过程，我们对时序图中所有有可能造成系统安全风险的过程进行展开和简化，RBC 切换过程中所有的不恰当控制行为化简结果如表 1 所示。经上述化简后，我们得到了 RBC 切换这个实际运营场景下有可能造成危险结果的不恰当控制行为。这些行为有具体的时点和错误的控制情况，设计人员在设计相关功能时，需要考虑这些时点的不安全行为，从而更好地保证系统安全。同时，在后期测试工作中，也应针对可能导致这些时点出现不恰当控制行为的情况予以考虑，从而更加周密的完成测试，提高测试效率。3 结束语传统安全分析方法受制于由故障组件开始的安全分析，多关注与具体的某个组件故障后对系统安全性的影响，本文给出了自上而下的控制行为辨识方式，辅以时序逻辑分析，在保证危险控制行为辨识准确性的同时，尽可能的考虑了控制行为间时序对不恰当控制行为的影响，并以 RBC 系统切换为例进行了分析，得出了 RBC切换运营场景下的具体不恰当控制，为安全系统设计者和安全系统测试者提供参考。参考文献1 刘金涛.基于 STPA 的需求阶段的高速列车运行控制系统安全分析方法研究 D.北京交通大学,2015.2 胡少强.基于 STPA 和有色 Petri 网的列控系统安全分析 D.北京交通大学,2018.3 TB/T 3530-2018 CTCS-3 级列车运行控制系统系统需求规范 S.4 TB/T 3510-2018 列控中心接口规范 S.5 TB/3330-2015 无线闭塞中心技术规范 S.作者简介林经源（1997-）(通讯作者)，男，回族，山东省人。硕士学历。研究方向为列控系统安全性分析。何涛（1977-）,内蒙古自治区人。铁路信号专业,教授。研究方向为轨道交通智能测试评估系统研究。图 3：CTCS-3 级列控系统分层控制系统模型图