自动控制文献翻译——摘要：SNCF负责法国铁路网计算机联锁系统的服务事项。因此SNCF很重要，特别对SIL4计算机联锁系统，SNCF有它自己的审批手续来确保新的联锁系统在法国铁路网环境中的安全。安全设备在交付使用前的检查和测试以及检查和测试的结果都是很必要的，随着时间的推移检查和测试结果可能会有变化。经济约束和计算机工具发展的复杂性都致使审批手续的性能遭到限制（人工或自动的）。验证覆盖率的减少会影响到具体实践应用。

本论文介绍的方法和工具使新计算机系统的验证和法国现有计算机联锁系统的改进，都可以通过实时多功能佩特里网进行。我们的目的就是向SNCF提供法国联锁系统验证的有效方法。本论文介绍的是一种被肯定了的论证方法，该方法应用于像计算机联锁系统这样的工业自动化设备，并且该方法的应用涵盖了工业自动化的规格和软件实现。通过该方法的提出并结合该方法的有关工具，我们可以随时证明系统的安全特性，并且不需要其他条件：该方法完全取代了室内检测（不是室外检测）。该方法不难在SNCF的检测程序中得到应用。

我们所期盼的最直接的好处就是测试时间和有关费用的降低，以及覆盖率的增加，还有对铁路基础设施建设的需求响应及计算机联锁系统的验证。让基层工程师掌握正规的验证方法可以证明更高的安全并不需要更多的花费。

关键字： 联锁系统 正规方法 正规验证 花销裁剪 安全 佩特里网

1.绪论

铁路风险分析的特点之一就是去分析出那些故障有很低的边缘概率，而这些危险项目是我们期望能够被发现和分析的（这是和相关系统普通模式相比较而言的）。因此，在法国铁路故障（失败，事故）数据的反馈是很少的。我们根据故障情况，将其定义为三种形式：

（1）故障特征；这种情况下有足够的故障数据，也就是非可编程系统；

（2）正常工作状态下的异常判别；在这种情况下，有用数据分布不相称；可编程系统应用较长时间；

（3）在有用的异常数据得不到反馈的情况下，运用统计法是不可行的。我们可以建立系统常规方式下的一种模型，在异常缺陷探测中可以应用该模型，也就是新的可编程系统或多功能系统。事实上，近来的数据表明统计学并不适用于计算机联锁系统功能的验证（SIL3或SIL4的功能）。

2.标准验证法与铁路行车安全

对于实时的计算机系统来说，区分如下两种不同是很不要的：

（1）各项功能必须通过系统来实现，而且必须翻译成计算机所熟悉的语言。在这种情况下，主要问题是规格和转换数据是否100%正确。很明显，对于一个高安全级别设备的应用，即使接受代码里的一个错误都会导致事故发生。经验告诉我们这种情况是存在的。

（2）系统的体系结构（硬件和软件）允许体统功能的安全度在一个容许的范围内（也就是安全故障修订的可容许故障）。在这种情况下的主要问题是在实际应用的系统框架中，最大残留错误的级别能否被检测出来。这涉及每小时的非安全错误率，包括当前模块及其限制内的系统运行错误。

对于第一部分，我们必须考虑到“以质量求发展”的方针，本身并不能保证该系统功能是“正确的”。该观点可通过欧洲铁路的实际经验得证。这就是为什么要引进正规方法来使铁路计算机使用中的故障维修花费最优化的原因。正规方法的优点是可在适当的时间内详细分析可编程系统的所有功能，以及确保被模型验证过的功能和实际系统的功能相吻合。随后......

ABSTRACT：SNCF is responsible for putting into service a interlocking systems on the French railway network. It is therefore essential, especially for computerized SIL4 systems that, SNCF has its own approval process to ensure that new interlocking systems are safe in the context of the French network. Checks and tests before putting safety facilities into service as well as the results of these tests are essential, time consuming and may show great variations between each other. Economic constraints and the increasing complexity associated with the development of computerized tools tend to limit the capacity of the classic approval process (manual or automatic). A reduction of the validation cover rate could result in practice.

The method and the tool presented in this paper makes it possible to formally validate new computerized systems or evolutions of existing French interlocking systems with real-time functional interpreted Petri nets. The aim of our project is to provide SNCF with an effective method for the formal validation of French interlocking systems. A formal proof method by assertion, which is applicable to industrial automation equipment such as interlocking systems, and which covers equally the specification and its real software implementation, is presented in this paper. With the proposed method and its associated tools we completely verify that the system follows all safety properties at all times and does not show superfluous conditions: it replaces all the indoor checks (not the outdoor checks). It can easily be included in the existing SNCF testing procedures.

The immediate advantages expected are a significant reduction of testing time and of the related costs, an increase of the test coverage rate, an answer to the new demand of railway infrastructure maintenance engineering to modify and validate computerized interlocking systems. Formal methods mastery by infrastructure engineers is surely a key to prove that more safety is not necessarily more expensive. 

Keywords: Interlocking system, Formal method, Formal validation, Costs reducing, Safety, Petri nets

1. INTRODUCTION

One of the particularities of railway risk analysis is that the hazard events that we wish to detect and to analyze have a very low marginal probability (they correspond to abnormalities in comparison to the regular mode of the concerned system). Consequently, feedback data of these hazard events (failures, accidents) in the French railway system are very rare.

We identify three types of problems, depending on what aspect one focuses on:

（1）characterization of hazard events; in this case there is adequate available data,  i.e. non-programmable systems;

（2）discrimination of the abnormalities from situations of normal working; in this case the strength of the available data will be strongly disproportionate, i.e. programmed systems in use for a long while;

（3）in the extreme case where no feedback data of abnormalities are available, it is not possible to use a statistical approach. One can construct a model of the regular modes of the system and this model can serve to detect the gaps corresponding to possible abnormalities i.e. new programmed systems or systems after functional modifications.In fact, recent accidents have shown that statistical approaches are......