ARINC 659通信总线的设计与实现
摘要
安全计算机平台作为安全苛求系统的重要部分,CBTC系统中区域控制器ZC和数据存储单元DSU的应用软件都加载在安全计算机平台上。ZC区域内的所有列车的车载控制器将列车的位置和速度信息发往安全计算机平台上的ZC应用程序。
常规通信所使用的硬件和软件看作黑色通道,信息在黑色通道中传输时可能导致错误或者故障的主要原因有随机错误、硬件故障和因软硬件问题而导致的系统失效,这些都会导致通信的安全风险,而且一个错误或者故障往往导致多个安全风险。安全计算机上承载的各种重要信息,要求系统不但要拥有高效、准确的运行能力,还需很高的通信安全性和可靠性。为了确保安全计算机平台数据安全,通信总线是关键因素。只有在通信总线可靠的基础上,研究技术实现的细节才有意义。
论文以航空总线ARINC 659航空背板通信总线协议标准为依据,分析了安全苛求系统的故障安全通信需求。通过对比各种通信总线的优缺点,选取了ARINC659航空背板通信总线协议标准作为本文设计的基础。在分析通信总线结构的基础上,设计并实现了基于ARINC 659的通信总线协议方案。
论文设计的通信总线是以高可靠性、时间确定性为重点。论文详细介绍了保证高容错性、和时间确定性调度策略的具体功能实现方法。以容错结构和双总线交叉检测方式来保证通信总线的高可靠性；以TDPA(表驱动比例访问机制)来保证了通信的时间确定性。
通信IP核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积,提高电路的稳定性,而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中,将通信IP核划分为不同的功能子模块,对每个子模块进行设计与实现,并且对仿真结果进行分析,保证其设计基本正确。
仿真验证只能保证通信IP核的仿真结果正确,为了避免存在潜在的设计错误,论文利用基于断言的方法(Property Specification Language, PSL)对通信IP核进行形式化验证,对其内部设计的正确性和完整性进行检验。如果断言失败,发现设计错误时,对检验出的设计错误进行分析、修改。再进行新的验证,直到形式化验证证明其设计没有潜在的设计缺陷为止。
论文结果表明,对于基于可编程逻辑设计的通信总线,利用断言对设计进行形式化验证,可以检验出仿真无法检验出的错误,保证其设计的完整性和正确性,从而得到一个无设计缺陷、可靠的通信总线。
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.
常规通信所使用的硬件和软件看作黑色通道,信息在黑色通道中传输时可能导致错误或者故障的主要原因有随机错误、硬件故障和因软硬件问题而导致的系统失效,这些都会导致通信的安全风险,而且一个错误或者故障往往导致多个安全风险。安全计算机上承载的各种重要信息,要求系统不但要拥有高效、准确的运行能力,还需很高的通信安全性和可靠性。为了确保安全计算机平台数据安全,通信总线是关键因素。只有在通信总线可靠的基础上,研究技术实现的细节才有意义。
论文以航空总线ARINC 659航空背板通信总线协议标准为依据,分析了安全苛求系统的故障安全通信需求。通过对比各种通信总线的优缺点,选取了ARINC659航空背板通信总线协议标准作为本文设计的基础。在分析通信总线结构的基础上,设计并实现了基于ARINC 659的通信总线协议方案。
论文设计的通信总线是以高可靠性、时间确定性为重点。论文详细介绍了保证高容错性、和时间确定性调度策略的具体功能实现方法。以容错结构和双总线交叉检测方式来保证通信总线的高可靠性；以TDPA(表驱动比例访问机制)来保证了通信的时间确定性。
通信IP核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积,提高电路的稳定性,而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中,将通信IP核划分为不同的功能子模块,对每个子模块进行设计与实现,并且对仿真结果进行分析,保证其设计基本正确。
仿真验证只能保证通信IP核的仿真结果正确,为了避免存在潜在的设计错误,论文利用基于断言的方法(Property Specification Language, PSL)对通信IP核进行形式化验证,对其内部设计的正确性和完整性进行检验。如果断言失败,发现设计错误时,对检验出的设计错误进行分析、修改。再进行新的验证,直到形式化验证证明其设计没有潜在的设计缺陷为止。
论文结果表明,对于基于可编程逻辑设计的通信总线,利用断言对设计进行形式化验证,可以检验出仿真无法检验出的错误,保证其设计的完整性和正确性,从而得到一个无设计缺陷、可靠的通信总线。
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.
引文
[1]燕飞.唐涛.轨道交通信号系统安全技术的发展和研究现状[J].中国安全科学学报.2005.15：94-99
[2]杨霓霏,段武,卢佩玲.铁路信号系统安全相关通信标准与安全协议研究[J].中国铁路.2008.6：48-51
[3]周治邦.故障安全和故障安全系统[J].铁道学报.2002.(24)：54-58
[4]张屹,魏学业,何春明.安全通信规范Subset-098的安全性分析[J].铁路通信信号Vol.45,No.11.2009.9：56-57
[5]王明志.开放环境中的安全通信[J].铁路通信信号工程技术.2009.8：14-16
[6]唐涛.燕飞.郜春海.轨道交通信号系统安全评估与认证体系研究[J].都市快轨交通.2004.17：74-79
[7]田小芳,赵大伟,谭永东.列车信息控制系统安全相关特性研究[J].铁路通信信号工程技术.2007.10：54-56
[8]余翔,谢长君等.车载网络FlexRay的研究与应用[J].电子元器件应用,2006：70-72
[9]黄雯,张浩等FlexRay总线技术及其多节点通信测试研究[J].东华电力,2009,37(1)：111-116
[10]袁吴昀,陈觉晓等.车载FlexRay网络管理策略的初步研究[J].单片机与嵌入系统应用,2008,5：20-21,28
[11]徐兰兰,孔令伟等FlexRay网络时滞特性分析[J].哈尔滨商业大学学报,2009,25(2)：195-198
[12]王婧,张欣.汽车网络通信协议TTP/C和FlexRay的研究分析[J].北京汽车,2006,6：40-43
[13]Alexander Merzner. Predictable and Efficient Architectures for Real Time System Synthesis.2005
[14]Kopetz H, Bauer G. The time-triggered architecture. Proceedings of the IEEE.2003
[15]Manuele Bertoluzzo, Giuseppe Buja. Investigation on the application of a time-triggered protocol aboard trains. Department of Electrical Engineering,2006,3685-3690
[16]王洪涛,基于时间触发机制的以太网在CBTC系统应用中的研究[硕士学位论文],2009
[17]徐文辉.ARINC659总线简介[J].航空电子技术,1999,2：22-27
[18]ARINC SPECIFICATION 659 BACKPLANE DATA BUS[A]. the Airlines Electronic Engineering Committee[C]. DEC.27,1993.
[19]马宁,李玲等ARINC659总线协议芯片的仿真验证[J].计算机技术与发展,2010,20(1)：205-208
[20]强新建,田泽,淮治华.基于ARINC659的FPGA原型验证平台的构建与实现[J].计算机工程与设计,2010,31(12)：2726-2728
[21]Brendan Hall, Kevin Driscoll, Michael Paulitsch. A New Ring Network For Superior Low-Cost Dependability. Computer society,2005
[22]韩俊刚.硬件设计的形式化验证[J].计算机研究与发展.1991.11：59-62
[23]王青,杨孟飞.基于断言的形式验证方法研究与应用[J].控制工程,2006,5：52-58
[24]"Open Verification Library Reference Manual", Accellera,California,2003
[25]"SystemVerilog 3.1, draft 2:Accellera's Extensions to Verilog", Accellera, California, 2003
[26]"Property Specification Language 1.0,Reference Manual",Accellera,California,2003
[27]Kausik Datta,P P Das."Assertion Based Verification Using HDVL"Proceedings of the 17th International Conference on VLSI Design(VLSID'04),Computer Society IEEE 2004
[28]郭亮,李玲等ARINC659总线接口芯片的FPGA原型验证[J].计算机技术与发展,2009,19(12)：240-247
[29]孟锐,张盛兵.ARINC659总线协议容错机制的一种设计与实现[J].航空计算技术,2008,38(6)：111-118
[30]李宝羽,张盛兵,安建峰ARINC659总线协议同步机制的研究与实现[J].航空计算技术,2009,39(2)：117-119
[31]仁爱锋.初秀琴.常存等.基于FPGA的嵌入式系统设计[M].西安.西安电子科技大学出版社.2004.10
[32]徐志军.徐光辉CPLD/FPGA的开发与应用[M].北京.电子工业出版社.2002
[33]甘历VHDL应用与开发实践[M].北京.北京科学出版社.2003
[34]王金明.杨吉斌.数字系统设计与Verilog HDL[M]北京.电子工业出版社.2002
[35]虞蕾,赵宗涛.PSL逻辑及验证技术研究进展与展望[J].计算机应用研究,2010,27(7)：2414-2420
[36]杨晓峰.林涛.用PSL语言进行基于断言的验证方法[J].电子设计应用.2005.12：89-90
[37]张倩.基于可编程逻辑的硬件平台的设计与形式化验证[硕士学位论文].北京交通大学.2009
[2]杨霓霏,段武,卢佩玲.铁路信号系统安全相关通信标准与安全协议研究[J].中国铁路.2008.6：48-51
[3]周治邦.故障安全和故障安全系统[J].铁道学报.2002.(24)：54-58
[4]张屹,魏学业,何春明.安全通信规范Subset-098的安全性分析[J].铁路通信信号Vol.45,No.11.2009.9：56-57
[5]王明志.开放环境中的安全通信[J].铁路通信信号工程技术.2009.8：14-16
[6]唐涛.燕飞.郜春海.轨道交通信号系统安全评估与认证体系研究[J].都市快轨交通.2004.17：74-79
[7]田小芳,赵大伟,谭永东.列车信息控制系统安全相关特性研究[J].铁路通信信号工程技术.2007.10：54-56
[8]余翔,谢长君等.车载网络FlexRay的研究与应用[J].电子元器件应用,2006：70-72
[9]黄雯,张浩等FlexRay总线技术及其多节点通信测试研究[J].东华电力,2009,37(1)：111-116
[10]袁吴昀,陈觉晓等.车载FlexRay网络管理策略的初步研究[J].单片机与嵌入系统应用,2008,5：20-21,28
[11]徐兰兰,孔令伟等FlexRay网络时滞特性分析[J].哈尔滨商业大学学报,2009,25(2)：195-198
[12]王婧,张欣.汽车网络通信协议TTP/C和FlexRay的研究分析[J].北京汽车,2006,6：40-43
[13]Alexander Merzner. Predictable and Efficient Architectures for Real Time System Synthesis.2005
[14]Kopetz H, Bauer G. The time-triggered architecture. Proceedings of the IEEE.2003
[15]Manuele Bertoluzzo, Giuseppe Buja. Investigation on the application of a time-triggered protocol aboard trains. Department of Electrical Engineering,2006,3685-3690
[16]王洪涛,基于时间触发机制的以太网在CBTC系统应用中的研究[硕士学位论文],2009
[17]徐文辉.ARINC659总线简介[J].航空电子技术,1999,2：22-27
[18]ARINC SPECIFICATION 659 BACKPLANE DATA BUS[A]. the Airlines Electronic Engineering Committee[C]. DEC.27,1993.
[19]马宁,李玲等ARINC659总线协议芯片的仿真验证[J].计算机技术与发展,2010,20(1)：205-208
[20]强新建,田泽,淮治华.基于ARINC659的FPGA原型验证平台的构建与实现[J].计算机工程与设计,2010,31(12)：2726-2728
[21]Brendan Hall, Kevin Driscoll, Michael Paulitsch. A New Ring Network For Superior Low-Cost Dependability. Computer society,2005
[22]韩俊刚.硬件设计的形式化验证[J].计算机研究与发展.1991.11：59-62
[23]王青,杨孟飞.基于断言的形式验证方法研究与应用[J].控制工程,2006,5：52-58
[24]"Open Verification Library Reference Manual", Accellera,California,2003
[25]"SystemVerilog 3.1, draft 2:Accellera's Extensions to Verilog", Accellera, California, 2003
[26]"Property Specification Language 1.0,Reference Manual",Accellera,California,2003
[27]Kausik Datta,P P Das."Assertion Based Verification Using HDVL"Proceedings of the 17th International Conference on VLSI Design(VLSID'04),Computer Society IEEE 2004
[28]郭亮,李玲等ARINC659总线接口芯片的FPGA原型验证[J].计算机技术与发展,2009,19(12)：240-247
[29]孟锐,张盛兵.ARINC659总线协议容错机制的一种设计与实现[J].航空计算技术,2008,38(6)：111-118
[30]李宝羽,张盛兵,安建峰ARINC659总线协议同步机制的研究与实现[J].航空计算技术,2009,39(2)：117-119
[31]仁爱锋.初秀琴.常存等.基于FPGA的嵌入式系统设计[M].西安.西安电子科技大学出版社.2004.10
[32]徐志军.徐光辉CPLD/FPGA的开发与应用[M].北京.电子工业出版社.2002
[33]甘历VHDL应用与开发实践[M].北京.北京科学出版社.2003
[34]王金明.杨吉斌.数字系统设计与Verilog HDL[M]北京.电子工业出版社.2002
[35]虞蕾,赵宗涛.PSL逻辑及验证技术研究进展与展望[J].计算机应用研究,2010,27(7)：2414-2420
[36]杨晓峰.林涛.用PSL语言进行基于断言的验证方法[J].电子设计应用.2005.12：89-90
[37]张倩.基于可编程逻辑的硬件平台的设计与形式化验证[硕士学位论文].北京交通大学.2009