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

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

改进的最小割集生成算法与联锁系统模型的安全性测试*

为保证铁路联锁模型的安全性,在故障分析法的基础上提出一种新的用Petri网来建立故障树的方法,动态地描述铁路联锁系统的安全性需求,并根据Petri网安全需求模型的可达标志图,提出一种能自动生成最小割集的算法。根据算法生成的最小割集,设计了一个联锁安全检测器,用于检测和控制联锁系统模型处于安全状态。最后用CPN工具对所建立的联锁系统模型进行仿真,仿真结果表明联锁安全检测器能够保证模型的安全性。     

Automated Verification of Signalling Principles in Railway Interlocking Systems

In this paper we present a verification strategy for signalling principles for the control of a railway interlocking system written in ladder logic. All translation steps have been implemented and tested on a real-world example of a railway interlocking system. The steps in this translation are as follows: 1. The development of a mathematical model of a railway interlocking system and the translation from ladder logic into this model. 2. The development of verification conditions guaranteeing the correctness of safety conditions. 3. The verification of safety conditions using a satisfiability solver. 4. The generation of safety conditions from signalling principles using a topological model of a railway yard.     

轨道交通联锁领域特定语言的形式化

作为轨道交通系统的核心子系统之一，对联锁系统进行形式化建模与分析，是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合，由于形式化知识难以掌握，领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题，针对联锁系统的故障随机性、行为实时性、构件可重用的特点，提出设计联锁领域特定语言IS-SDL描述具体的联锁系统的参数，并基于随机混成自动机模板自动生成联锁系统的形式化模型，以进一步在此基础上进行安全分析.首先对联锁系统模型进行分析，根据不同案例设计其领域特定语言；其次，确定联锁系统的系统模型的模板，包括环境构件模板和控制器模板，并举例抽取其随机混成自动机模板；在模板基础上定义系统模型生成过程，让领域专家可以通过领域特定语言，输入参数自动生成具体的随机混成自动机系统模型；最后以某站联锁系统为例，展示了基于模板的具体系统模型的生成过程，并通过基于系统模型的事故预测分析，证明了该方法的可行性与有效性.     

Case Study: Formal Verification of a Computerized Railway Interlocking

We describe a case study in system-level verification of a computerized railway interlocking developed by ADtranz Spain, installed and put into test use at a subway station in Madrid. The formal modelling and analysis was carried out by personell at ADtranz Sweden using a tool for automatic formal modelling of the interlocking system and the commerical verification software NP-Tools, which is based on St?lmarck's patented proof procedure. The case study took about one man week in total, of which most of the time was spent modelling safety requirements. The analysis discovered an error that had passed the traditional verification phase. The actual analysis time, disproving the safety requirements by supplying a countermodel, was done in a matter of seconds. The corrected software could be proved to fulfil the safety requirements in the same amount of time. This case study is one of many carried out by ADtranz during 1995-98 in the process in which they have replaced the traditional techniques used for system level verification of safety with formal techniques. We give an overview of the formal methods and tools used which today are integrated in the development environment at ADtranz. Received March 1997 / Accepted in revised form July 1998     

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。     

容错计算机联锁系统

容错计算机联锁系统是使用容错计算机构成的车站计算机联锁系统,其基本思想是：通过TMR的硬件冗余方式,实现系统的高可靠性和高安全性.该文将介绍我国两种典型的容错计算机联锁系统(TYJL&TR9、DS6&20型),并对其可靠性和安全性进行定量的分析.     

基于有向图的进路搜索算法研究与设计

进路搜索是铁路车站计算机联锁系统的基本功能,其运行效率及所得目标进路的安全性对于保证行车安全意义重大。本文通过对铁路车站站场图与有向图的相似性进行研究,建立其网络拓扑结构与节点模型,结合深度优先遍历算法和搜索约束条件,提出一种适用于铁路车站实际情况的进路搜索算法,并给出了完整的描述。     

基于Petri网的联锁软件测试用例动态生成

根据Petri网可动态描述和分析系统行为的特性,设计铁路计算机联锁软件安全需求Petri网模型,进而提出基于Petri网故障树的最小割集求解算法以及基于形式化故障树最小割集的测试用例动态生成算法。虚拟站场上的测试结果表 明,该方法能有效地降低测试过程的资源消耗,提高软件测试的效率,为联锁软件的设计与改进提供测试依据。     

PLC构成PROFIBUS网络原理及应用

微机联锁系统中,一般是将联锁置于上位机中,这样安全性、可靠性得不到保障。文中用西门子S7-400HPLC完成联锁功能,构成PROFIBUS-DP/MPI分布式网络系统,这样整个联锁系统安全可靠。通过介绍DP/MPI网的概念和实现,结合唐山钢铁公司焦化站联锁实例,着重阐明用PLC实现DP/MPI网络,以解决该联锁系统中分布式输入输出等。经现场调试、安装,整个网络运行良好,安全可靠地实现和完成车站信号联锁系统的联锁功能,应用前景很好。     

人工干预条件下多媒体联锁仿真研究

提出了人工干预条件下基于站场图的多媒体联锁仿真模型,给出了铁路站场信息和联锁关系的多媒体表达,解决了分散自律调度集中系统仿真环境研发的关键问题,实践证明,该模型符合仿真环境要求,效果良好。     

基于场景分析的系统形式化模型生成方法

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。     

Efficient formalization of railway interlocking data in RailML

Railways wish to reduce the costs of engineering interlocking systems by simplifying the exchange of technical information between stakeholders. Exchanging interlocking data in a machine-readable and standardized format removes inefficiency due to misinterpretation and conversion of data from non-standard, often paper-based formats. This paper proposes an UML class representation of the interlocking data that maps the characteristics of the interlocking system. These data model represents both tabular and geographical interlocking. The model reflects the topology of the railway network that the interlocking controls, routes, relations between signal aspects, speed indication signals, automatic train protection (ATP) and the state of movable and non-movable track elements. The data are machine-readable RailML, an incarnation of XML that is gaining the status of standard in railway modelling. We applied our approach to model the Dutch Santpoort Noord station, starting from paper-based track and signal plans. The resulting database captures all the features of the interlocking, whilst removing data redundancy. The model has general validity and it is easily extendible to other interlocking and ATP systems. Our approach contributes to create standard, electronic interlocking databases, directly from technical documents currently used in the practical world.     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

基于Petri网的联锁软件安全性测试的研究

安全是铁路运输生产永恒的主题。联锁软件是保障铁路车站列车或机车(以下简称列机车)作业安全的关键软件,充分的测试对于保证其安全性具有举足轻重的作用。文章在分析文献[1][5][6]的联锁软件安全性需求故障树模型的基础上建立了联锁软件安全性需求的Petri网模型,提出了一种基于十字链表的Petri网的存储结构,给出了一种求解割集的算法实现;接着简述了安全性测试用例的自动生成方法;最后给出了该方法在HJ04A系统联锁软件安全性测试中的应用。     

嵌入式联锁控制器软件体系结构动态建模研究

首先应用π演算和Petri网的相关理论,建立了嵌入式联锁控制器软件体系结构抽象模型ISAM;然后对ISAM模型的动态演化、一致性和死锁进行了深入研究;最后应用ISAM抽象模型,对嵌入式联锁控制器软件系统进行分析。     

面向安全苛求软件的测试用例自动生成*

测试用例的自动生成是验证安全苛求软件最关键的技术问题,然而目前的研究并没有充分考虑安全苛求软件的安全性需求,为此提出一种应用安全覆盖准则的安全苛求软件的测试用例自动生成策略,将该策略应用于铁路车站计算机连锁软件,并与全节点覆盖准则进行了比较。结果表明该策略对关键变迁有更高的安全性保证。     

DCS系统在硫酸余热发电过程中的应用

本文简述了硫酸余热发电的工艺流程，及工艺对系统控制的要求，并用DCS系统实现对硫酸厂、脱盐水站、废热锅炉、汽轮机、发电机等的重要参数进行检测，对锅炉汽包、主蒸汽等实施有效控制，及用联锁控制确保系统正常安全运行的方法。     

基于RTLinux的计算机联锁软件可靠性和实时性研究

采用性能稳定、可靠性高、实时性好的RTLinux作为联锁计算机的操作系统,可以有效地提高计算机联锁软件的可靠性和实时性.叙述了对软件可靠性的描述和提高系统软件可靠性的具体方法,以及RTLinux的实时性,在RTLinux平台下的IPC机制,并进行了相应的测试.     

A logic approach to decision taking in a railway interlocking system using Maple

Railway interlocking systems are apparatuses that prevent conflicting movements of trains through an arrangement of tracks. A railway interlocking system takes into consideration the position of the switches (of the turnouts) and does not allow trains to be given clear signals unless the routes to be used by the trains do not intersect. A new model, based on Boolean Logic, and independent from the topology of the station is presented in this paper. According to this new model, any given proposed situation is safe if and only if a certain set of formulae (translating the position of trains and the movements allowed - the latter depend on the position of the switches and the colour of the semaphores) is consistent. The main procedure analyses the safety of a proposed situation and returns, if they exist, the sections where a collision could take place. The fact that trains could occupy more than one section is considered. The code of the corresponding Maple implementation is surprisingly brief.