一个协议的形式化规范与验证开题报告

全文总字数：1848字

1. 研究目的与意义

现如今计算机正被应用于越来越广泛的领域，其中一个重要的领域就是生命攸关系统。

所谓生命攸关系统是指一个系统的失效或误操作会产生人员重伤甚至死亡或者设备的严重损坏或对环境的危害，例如航空控制系统。

这类的风险一般会配合安全工程的工具进行管理。

2. 国内外研究现状分析

作为重要的航空协议，ARINC 653自发布以来就因其广阔的应用前景而受到大量关注和研究。

赵永望等研究者采用集成主体和求精的方法对ARINC 653协议的分区操作系统进行形式化地规范和分析，并力求建立形式化方法与非形式化方法之间的中间模型；Laura Carnevali等研究者则通过形式化的方法设计和验证ARINC 653协议的2级进程调度器；David Sanan等研究者则基于ARINC 653协议进行基于事件的生命攸关系统的形式化研究；在本文参考文献中，Artur Oliveira Gomes用形式化的方法规范和验证了ARINC 653协议中操作系统的核心部分，其中包括ARINC 653协议中的分区层，操作系统接口层（APEX层）以及操作系统层的主干部分，协议中的其他部分则尚未规范和验证，例如其中操作系统层中的分区调度，时间管理，分区间交互以及分区中的进程管理和健康监视器等等。

3. 研究的基本内容与计划

本毕业设计的内容：用形式化语言circus规范arinc 653协议中的health monitor。

具体细节如下： 1) 熟悉arinc 653协议和其health monitor相关的部分。

2)用形式化语言把health monitor的性质和服务描述出来。

4. 研究创新点

本文采用形式化的方法对ARINC 653协议中Health Monitor的部分进行规范，并能够确保规范出的Health Monitor部分能够满足ARINC 653协议的要求，相比以往的软件工程的方法，具备更高的正确性和可靠性，而且也为具体代码的实现提供了指导；在形式化规范的同时，也考虑到了后续具体代码的实现，也留意了代码的重用，降低代码冗余的同时提高开发和运行的效率。