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