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

摘要

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

目录

文摘

英文文摘

声明

致谢

1 绪论

1.1 选题的目的和意义

1.2 安全硬件平台的研究情况

1.2.1 故障安全概念

1.2.2 安全计算机发展情况

1.3 形式化验证

1.3.1 形式化验证方法分类

1.3.2 基于断言的模型检验

1.3.3 断言方法的确定

1.4 论文的研究内容和组织结构

1.5 本章小结

2 安全硬件平台系统结构设计

2.1 安全计算机结构分析

2.1.1 安全苛求系统对硬件平台的要求

2.1.2 常见安全硬件平台结构

2.1.3 我国铁路的计算机联锁系统结构

2.2 几种二取二安全计算机结构比较

2.2.1 双通道双处理器锁步结构

2.2.2 双套算法的二乘二取二安全平台结构

2.2.3 单板双机嵌入式容错系统

2.3 取二安全硬件平台设计

2.3.1 CBTC系统中安全硬件平台的功能要求

2.3.2 取二安全硬件平台结构设计

2.3.3 取二安全硬件平台接口

2.4 本章小结

3 安全硬件平台功能设计

3.1 安全性设计

3.1.1 安全硬件平台同步方式

3.1.2 安全硬件平台数据比较方式

3.2 通用性设计

3.2.1 处理器要求

3.2.2 数据帧结构和控制字

3.2.3 处理器与比较核的接口格式

3.3 应用软件调度策略

3.4 安全比较核设计

3.5 本章小结

4 基于可编程逻辑的安全比较核设计

4.1 使用工具和设计方法介绍

4.1.1 FPGA的结构和特点

4.1.2 VHDL的特点

4.2 安全比较核的总体方案

4.3 各功能模块的设计与实现

4.3.1 数据接收、校验模块的设计与实现

4.3.2 数据比较模块的设计与实现

4.3.3 比较结果审核、自检模块的设计与实现

4.3.4 同步模块的设计与实现

4.4 模块的仿真结果分析

4.4.1 数据接收、校验模块的仿真结果分析

4.4.2 数据比较模块的仿真结果分析

4.4.3 比较结果审核、自检模块的仿真结果分析

4.4.4 同步模块的仿真结果分析

4.5 本章小结

5 安全比较核的形式化验证

5.1 基于PSL的断言

5.1.1 PSL概述

5.1.2 PSL断言的实现结构

5.1.3 基于PSL进行形式化验证的流程

5.2 基于PSL的安全比较核功能验证

5.2.1 断言的必要性

5.2.2 安全比较核重点模块的断言方案

5.2.3 断言执行步骤举例分析

5.2.4 断言的执行情况分析

5.3 本章小结

6 结论和展望

参考文献

作者简历