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