基于SPIN的命题投影时序逻辑模型检查

摘要

目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造正确可靠的系统。为了达到上述目标，形式化方法在软件开发中得到了广泛的应用，特别是模型检查技术。 本文提出了一种基于SPIN的命题投影时序逻辑的模型检查方法。 在此方法中，系统的性质用命题投影时序逻辑公式来描述，随后这个公式被转换为其永非断言； 然后系统模型用Buchi自动机来刻画； 最后通过SPIN完成模型检查，即检查系统是否满足期望的性质。 为了实现这一目的，文中设计并实现了命题投影时序逻辑公式的解释转换器，以便将命题投影时序逻辑公式自动转换为Promela形式的永非断言。该转换器首先将待验证的命题投影时序逻辑公式转换为其正则式以及正则图，然后通过正则图可以得到所需的永非断言。将该转换器与模型检查器SPIN相结合，使用命题投影时序逻辑公式来在SPIN中描述系统的性质，这样基于命题投影时序逻辑的模型检查就能在SPIN中完成。

目录

文摘

英文文摘

声明

第一章 绪论

1.1研究背景

1.1.1存在的问题

1.1.2本文的研究方向

1.2研究现状

1.2.1模型检查技术研究现状

1.2.2时序逻辑研究现状

1.3本文的研究工作和章节安排

第二章 模型检查

2.1模型检查原理

2.2模型检查的主要方法

2.3模型检查技术的优点及局限性

2.3.1模型检查技术优点

2.3.2模型检查技术的局限性

2.3模型检查系统SPIN

第三章 命题投影时序逻辑

3.1语法

3.2语义

3.3可满足性和有效性

3.4导出公式

3.5优先级规则

3.6等价关系

第四章 命题投影时序逻辑的模型检查

4.1模型检查PPTL公式方案设计

4.2 PPTL公式的正则式

4.2.1 PPTL公式的正则式

4.2.2 PPTL正则式的转换算法

4.3 PPTL公式的正则图

4.3.1正则图的定义

4.3.2正则图的构造算法

4.4模型检查器设计与实现

4.4.1转换器的总体结构

4.4.2公式词法语法分析

4.4.3正则式转换模块设计

4.4.4正则图转换模块设计

4.4.4永非断言转换模块设计

第五章 NeedHam-Schroeder协议验证

5.1 NeedHam-Schroeder协议介绍

5.2 NeedHam-Schroeder协议验证

5.2.1 NeedHam-Schroeder协议的模犁

5.2.2 NeedHam-Schroeder协议的性质验证

结束语

致谢

参考文献

作者在读期间研究成果