【作者】 刘海旭；

【导师】 马连川；

【作者基本信息】 北京交通大学 ， 交通信息工程及控制， 2010， 硕士

【摘要】 安全计算机平台作为安全苛求系统的重要部分,CBTC系统中区域控制器ZC和数据存储单元DSU的应用软件都加载在安全计算机平台上。ZC区域内的所有列车的车载控制器将列车的位置和速度信息发往安全计算机平台上的ZC应用程序。常规通信所使用的硬件和软件看作黑色通道,信息在黑色通道中传输时可能导致错误或者故障的主要原因有随机错误、硬件故障和因软硬件问题而导致的系统失效,这些都会导致通信的安全风险,而且一个错误或者故障往往导致多个安全风险。安全计算机上承载的各种重要信息,要求系统不但要拥有高效、准确的运行能力,还需很高的通信安全性和可靠性。为了确保安全计算机平台数据安全,通信总线是关键因素。只有在通信总线可靠的基础上,研究技术实现的细节才有意义。论文以航空总线ARINC 659航空背板通信总线协议标准为依据,分析了安全苛求系统的故障安全通信需求。通过对比各种通信总线的优缺点,选取了ARINC659航空背板通信总线协议标准作为本文设计的基础。在分析通信总线结构的基础上,设计并实现了基于ARINC 659的通信总线协议方案。论文设计的通信总线是以高可靠性、时间确定性为重点。论文详细介绍了保证高容错性、和时间确定性调度策略的具体功能实现方法。以容错结构和双总线交叉检测方式来保证通信总线的高可靠性；以TDPA(表驱动比例访问机制)来保证了通信的时间确定性。通信IP核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积,提高电路的稳定性,而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中,将通信IP核划分为不同的功能子模块,对每个子模块进行设计与实现,并且对仿真结果进行分析,保证其设计基本正确。仿真验证只能保证通信IP核的仿真结果正确,为了避免存在潜在的设计错误,论文利用基于断言的方法(Property Specification Language, PSL)对通信IP核进行形式化验证,对其内部设计的正确性和完整性进行检验。如果断言失败,发现设计错误时,对检验出的设计错误进行分析、修改。再进行新的验证,直到形式化验证证明其设计没有潜在的设计缺陷为止。论文结果表明,对于基于可编程逻辑设计的通信总线,利用断言对设计进行形式化验证,可以检验出仿真无法检验出的错误,保证其设计的完整性和正确性,从而得到一个无设计缺陷、可靠的通信总线。更多还原

【Abstract】 As an important part of safety critical system, safe computing platforms have been loaded some application software, such as Zone Controller (ZC) and Data Service Unit (DSU). Vehicle on-board controllers of all trains within the bounds of ZC send train position and speed to ZC application program on safe computing platforms.Hardware and software for conventional communications are considered as black channel. When information transmitted in black channel caused errors or failures, the main reasons are random errors, hardware failures and system failures caused by hardware problems, which can lead to communication security risk, and an error or failure often leads to more security risks. Variety of important information on safe computer not only requires the system to have efficient and accurate operational capabilities, but also needs high communication security and reliability. Communications bus is a key factor to ensure data security on safe computing platforms. Only base on reliable communication bus, it is meaningful to research the implementation of technical details.Based on communication bus protocol standards of aviation backplane in ARINC Specification 659, the paper analyzes the needs of fail-safe communications of safety critical system. By comparing the advantages and disadvantages of various communication buses, ARINC Specification 659 is selected as the basis for this article. Protocol programs based on ARINC 659 are designed and realized in the basis of analyzing communication bus architecture.Communication bus is focus on high reliability time deterministic. The way to implementation of specific functions of scheduling strategy to ensure high fault tolerance and time deterministic is given in detailed in this paper. Fault-tolerant structure and dual bus cross-monitoring is to ensure high reliability of the communication bus, TDPA(Table Driven Proportional Access) is to ensure time deterministic of communication.Communication IP core is designed and realized based on programmable logic, which not only reduces the volume of circuit and improves the stability of the circuit, but also greatly reduces the design and debugging cycles of the whole system by this advanced development tools. In the implementation process, communication IP core is divided into different functional sub-module, by design and implementation of each sub-module and analysis of simulation results to ensure the basic correctness of design.The simulation can only ensure the result correct. The formal verification of the platform is based on assert by PSL (Property Specification Language). In order to avoid the potential design errors, use PSL to validate communication IP core, make formal verification of the validity and integrality of the compare core design. When the assert fail, the error can be detected. Analyze the error and modify the design, then simulate it again. After simulation, make formal verification again, until there is no potential design error.The paper shows that, for the design of communication bus based on programmable logic, it can test out the mistakes that the simulation can not discover by the use of assertions for formal verification in design and ensure the completeness and correctness of design, finally, a no design flaws and reliable communication bus is obtained.更多还原