区域控制器的安全需求建模与自动验证

轨道交通区域控制器（ZC）是我国轨道交通信号系统选型的主流制式——基于通信的列车控制系统（CBTC）的核心子系统，其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是ZC自身的复杂性以及领域知识的繁杂难以掌握，使得形式化方法很难应用到安全需求的验证中去.针对这些问题，提出一种安全需求的自动验证方法，使用半形式化的问题框架方法（PF）来建模和分解安全需求，根据需求模型自动生成安全需求的验证模型和验证性质，在此基础上自动生成验证模型的Scade语言实现，并通过Design Verifier验证器对需求进行组合验证.最后，使用了某个实际案例ZC的一个子问题CAL_EOA进行了研究，实验结果证明了该方法的可行性与有效性，它能自动地将安全需求模型进行组合验证，改善了验证的效率.     

车站联锁进路控制逻辑的形式化方法

基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法 Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行了形式化规范和推理,该模型在RODIN平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。     

车载TBTC-CBTC系统降级场景下的CPN建模与仿真

基于轨道电路的列车控制（TBTC）-基于通信的列车控制（CBTC）双模车载系统是实现轨道交通多网融合的关键,其模式间切换具有较强的随机性和并发性,并直接影响车载信号系统的运营可用性。然而,车载信号系统故障降级导致轨道交通资源利用率降低,表现为列车追踪的时间间隔增加,而间隔增加程度取决于区间长度和TBTC列车占用检测区段长度。从不同模式下资源分配、使用和释放角度,在列车运行过程中利用有色Petri网对TBTC-CBTC双模冗余车载信号系统的列车追踪运营场景进行建模,模拟CBTC车载信号系统故障发生的随机性和系统降级对后续列车的影响,精准描述并分析列车运营受影响的情况。将城市轨道交通项目的典型配置参数代入到有色Petri网模型中进行仿真,验证在不同线路下运营间隔受模式切换影响的程度。仿真结果表明,当区间长度小于1 500 m时,列车晚点时间可控制在180 s以内,晚点时间随着区间长度的增加而延长。     

浅谈无线CBTC与传统列控系统的比较及其优势

当今在轨道交通列车控制系统中,主要采用了传统基于轨道电路的列车控制系统。本文在系统的可靠性、行车追踪间隔、设备维护和管理、信息传输方式等方面进行分析比较。提出无线CBTC移动闭塞系统代表了轨道交通列车控制系统的发展方向。     

安全协议中的形式化验证技术

伴随着网络和通信的迅速发展,安全已经成为一个备受关注的问题,为确保不同系统的安全,出现了许多的安全协议.文中描述了安全协议验证的形式化需求,并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点,探讨了形式化验证技术所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向.     

可信编译器构造的翻译确认方法简述

编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。     

LTE-M系统的通信时延分析

下一代轨道交通采用LTE-M系统承载多种业务,并根据列车控制要求限定数据在较低的时延内完成传输。分析了列车移动终端接入基站的多种时延,对LTE-M相关协议产生的接入时延进行研究,将多信号并发时的接入化为排队论体系中的M/M/1/m/m模型,推导了传输时延的预测方法,并在LTE-M系统3MHz带宽专用承载CBTC业务的典型应用情况下的传输时延进行了预测,该计算方法可为今后同类通信系统传输低时延需求业务的设计提供参考。     

列车安全距离控制形式化建模与验证

随着我国铁路的迅速发展,对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题,以Event-B形式化仿真工具Rodin为基础,通过结合多智能体理论,引入感知决策法则,实现了无线闭塞中心(RBC)与列车的车地通信,建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行,对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明,对于CTCS列车控制系统的复杂逻辑关联行为,采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法,可进行系统规范的模型验证,对于复杂系统的逻辑验证有较强的实际意义。     

列车安全距离控制形式化建模与验证

随着我国铁路的迅速发展,对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题,以Event-B形式化仿真工具Rodin为基础,通过结合多智能体理论,引入感知决策法则,实现了无线闭塞中心(RBC)与列车的车地通信,建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行,对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明,对于CTCS列车控制系统的复杂逻辑关联行为,采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法,可进行系统规范的模型验证,对于复杂系统的逻辑验证有较强的实际意义。     

基于二维结构熵的CBTC系统信息安全风险评估方法

随着计算机技术、通信技术和控制技术在城市轨道交通列车运行控制系统中的应用，城市轨道交通的自动化和信息化程度不断提升.然而，基于通信的列车运行控制（Communication-based train control，CBTC）技术采用的通用计算机设备和通信技术带来的信息安全漏洞，给CBTC系统带来了日益严峻的信息安全风险，因此，对CBTC系统的信息安全风险进行量化、动态评估具有重要意义.本文根据设备及通信链路的差异性构建了CBTC网络拓扑模型，结合信息安全风险下线路列车运行性能变化导致的运能损失，采用综合表征信息域和物理域特征的二维结构信息熵对CBTC系统信息安全风险进行建模分析.最后，基于城市轨道交通列控系统半实物仿真平台对评估方法进行验证，表明所提方法对CBTC系统信息安全量化评估的有效性和准确性.     

可信系统性质的分类和形式化研究综述

计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.     

Systems engineering principles for the design of biomedical signal processing systems

Systems engineering aims to produce reliable systems which function according to specification. In this paper we follow a systems engineering approach to design a biomedical signal processing system. We discuss requirements capturing, specification definition, implementation and testing of a classification system. These steps are executed as formal as possible. The requirements, which motivate the system design, are based on diabetes research. The main requirement for the classification system is to be a reliable component of a machine which controls diabetes. Reliability is very important, because uncontrolled diabetes may lead to hyperglycaemia (raised blood sugar) and over a period of time may cause serious damage to many of the body systems, especially the nerves and blood vessels. In a second step, these requirements are refined into a formal CSP‖ B model. The formal model expresses the system functionality in a clear and semantically strong way. Subsequently, the proven system model was translated into an implementation. This implementation was tested with use cases and failure cases.Formal modeling and automated model checking gave us deep insight in the system functionality. This insight enabled us to create a reliable and trustworthy implementation. With extensive tests we established trust in the reliability of the implementation.     

应用ETDFA生成CBTC联锁软件形式化模型的方法

CBTC系统的联锁软件为SIL4级的高安全、高可靠软件,目前广泛使用的软件测试和仿真验证的结果严重依赖选取的测试向量,要保证高覆盖率的测试十分困难;EN50128中强烈推荐SIL4等级的软件使用形式化方法完成软件需求规格说明书和软件设计,因此,采用形式化的方法设计软件,是构造高可靠、高安全软件的一个重要途径;总结了现有的CBTC系统中联锁子系统集成方式及优缺点,并使用事件确定有限自动机ETDFA(event deterministic finite automata)模型对适用性更优的升级型集成方式的联锁软件的联锁逻辑完成形式化定义,保证联锁逻辑的正确性,减少软件的不确定性描述;以办理进路为例生成联锁对象的ETDFA模型,验证该方法的有效性和可行性;该方法不仅为CBTC联锁软件的设计与开发提供新思路,而且有助于安全苛求软件的形式化验证与分析,提高联锁软件的安全性和正确性。     

共识协议的形式化验证研究现状与展望

分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.     

From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions

Communications-based train control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent, scope, number, and even names of the implemented functionalities. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. This paper presents the results of an experience in defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The paper also describes a methodology to derive novel CBTC products from the global model, and to define system requirements for the individual CBTC components. To this end, the proposed methodology employs scenario-based requirements elicitation aided with rapid prototyping. To enhance the quality of the requirements, these are written in a constrained natural language (CNL), and evaluated with natural language processing (NLP) techniques. The final goal is to go toward a formal representation of the requirements for CBTC systems. The overall approach is discussed, and the current experience with the implementation of the method is presented. In particular, we show how the presented methodology has been used in practice to derive a novel CBTC architecture.     

Handling advanced scheduling heuristics under a hardware compiler generation environment

The complexity of modern digital systems requires complex design entry methods and thus, language based designs are often an appealing alternative for schematics. Language based design entry, supports high-level design transformations through formal and executable traditional compiler construction problem specifications, their main advantages being modularity and declarative notation. In this paper, this idea is exploited under a powerful compiler construction system and a methodology is given to design formal and executable high-level hardware manipulators. In effect, this methodology stands as a meta-level between hardware transformations and their implementation and can be valuable in fast evaluation of new ideas and techniques.     

跨系统可信互联安全体系研究

各部门及行业信息系统之间互联互通已成为我国信息化建设进一步深入发展的主题之一。本文提出通过建立可信互联平台,在实现跨系统互联的同时,保障信息交换和共享过程中各信息系统的信息网络安全。文中就跨系统可信互联的范围和目标进行了定义,提出和设计了可信互联平台安全体系,建立了安全体系实现框架,并对其中的边界防护机制和安全数据交换机制进行了论述。该安全体系已在实际应用中初步实现并取得了良好效果。     

Formal methods for railway control systems

The term intelligent transportation systems (ITS) refers to information and communication technology (applied to transport infrastructure and vehicles) that improve transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. The importance of ITS is increasing as novel driverless/pilotless applications are emerging. This special issue addresses the application of formal methods to model and analyze complex systems in the context of ITS and in particular in the field of railway control systems. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards.