基于可编程逻辑的硬件平台的设计与形式化验证

发布时间：2020-07-18 21:51

【摘要】： 安全硬件平台通过先进的计算机、电子技术来现实。随着计算机、电子技术的迅猛发展,系统性能大大提高,结构也变得越来越复杂。安全硬件平台作为安全苛求系统的重要部分,其安全性是至关重要的。在设计阶段就应充分考虑安全性,以免由于潜在的设计缺陷导致整个系统存在安全隐患。由于系统逐渐向规模大、性能强、复杂性高的方向发展,单纯利用仿真、测试等方法无法对系统进行无穷验证,因此在硬件平台设计阶段,利用形式化方法对硬件平台设计的正确性和完备性进行验证。 论文以基于通信的列车控制(Communication-based Train Control,CBTC)系统为应用背景,详细分析了安全硬件平台需求。通过对比各种平台结构的优缺点,选取了二乘二取二结构为本文设计的总体结构。在分析各种安全计算机结构的基础上,结合CBTC系统对安全硬件平台的功能需求,提出一种新的二取二系统结构方案。 论文设计的安全硬件平台是以安全性、通用性为重点。论文详细介绍了保证安全性、通用性和调度策略的具体功能实现方法。以微同步和硬件数据比较方式来保证平台的安全性;以处理器的约束、数据帧结构的确定和接口格式的固定来保证了平台的通用性。 安全硬件平台中的重要单元是安全比较核。安全比较核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积,提高电路的稳定性,而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中,将安全比较核划分为不同的功能子模块,对每个子模块进行设计与实现,并且对仿真结果进行分析,保证其设计基本正确。 仿真验证只能保证比较核的仿真结果正确,但对于复杂系统,无穷尽的仿真是不现实的。为了避免存在潜在的设计错误,论文利用基于断言的方法(PropertySpecification Language,PSL)对安全比较核进行形式化验证,对其内部设计的正确性和完整性进行检验。当断言失败,发现设计错误时,对检验出的设计错误进行分析、修改。再进行新的验证,直到形式化验证证明其设计没有潜在的设计缺陷为止。 论文结果表明,对于基于可编程逻辑设计的安全硬件平台,利用断言对设计进行形式化验证,可以检验出仿真无法检验出的错误,保证其设计的完整性和正确性,从而得到一个无设计缺陷、通用的安全硬件平台。
【学位授予单位】：北京交通大学
【学位级别】：硕士
【学位授予年份】：2009
【分类号】：TP302
【图文】：

机仍会继续运行下去，如果到下一个同步点仍然失步，且在连续的五次同步中失步三次，则表示双机完全失步，通过安全比较核对系统进行失步处理。同步处理过程如图3一2所示。同步开始\\N}司步1-卜二一同步2，)卜同步3同步2卜同步3同步4N同步3沐卜同步4同步5\)失步失步失步YY一丫下一v-}暨i」一同步…图3一2同步处理过程Fig.3一25 担chronizationexecutiveProeess从安全性和可用性的角度分析，这种方法在任务同步的基础上添加了时间片检测点同步，提高了系统的安全性，弥补了反应时间不足的缺点，同时也容忍了瞬时故障所造成的失步，使系统的可用性大大提高。任务同步检测点由处理器内部程序控制，时间片同步检测点由外部安全比较核控制，处理器和比较核各自记录同步历史数据，这样可以防止一方出现故障所导致的系统同步故障，或者出现同步检测故障，使系统出现危险输出。3.1.2安全硬件平台数据比较方式数据比较是二取二系统中保证安全的重要措施

匕京交通大学硕十学位论种可编程电路是:可编程逻辑块 (ConfigurableLogicBlock，cLB)、输入/输出模块(I/oBloek，IoB)和互连资源(IntereoimectResource，IR)，其基本的结构图如图4一l所示。墉 墉墉…烈 烈洲 洲 … …口 口… … 一一一一一一一一一一一一一一一一一一一一一一一一一一一一一;蒙 -----------------------------------------------------黛黛篡黔 黔 黔一卡斗一 一油睡 睡‘一羹翻禽入从犷 ---一斗一十一 一 一嚼冷 冷立 立立立立姗扛 扛 扛__二:轰 ___~-‘氦一 一一一一 甲舞哪哪 哪全 全 全 全 全 全全彻让 让 让。一;才、 、犯 犯 犯 犯犯犯犯犯犯 犯犯犯 犯 犯 犯犯犯犯犯犯犯 犯 犯 犯

PSL结构

【引证文献】

相关期刊论文 前1条

1 刘明端;穆建成;马连川;尚麟宇;;基于模型的安全比较核设计[J];沈阳建筑大学学报(自然科学版);2011年04期

相关硕士学位论文 前1条

1 刘海旭;ARINC 659通信总线的设计与实现[D];北京交通大学;2010年

本文编号：2761472