计算机系统形式化验证中的模型检测方法综述

《计算机系统形式化验证中的模型检测方法综述》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、计算机系统形式化验证中的模型检测方法综述1　形式化方法概述　　形式化方法是用数学和逻辑的方法来描述和验证系统设计是否满足需求。它将系统属性和系统行为定义在抽象层次上，以形式化的规范语言去描述系统。形式化的描述语言有多种，如一阶逻辑，Z语言，时序逻辑等。采用形式化方法可以有效提高系统的安全性、一致性和正确性，帮助分析复杂系统并且及早发现错误。形式化验证是保证系统正确性的重要方法，主要包括以数学、逻辑推理为基础的演绎验证(deductive　verification)和以穷举状态为基础的模型检测(model　checking)。演绎验证是基于人工数学来证明系统模型的正确性

2、。它利用逻辑公式来描述系统，通过定理或证明规则来证明系统的某些性质。演绎验证既可以处理有限状态系统，又可以解决无限状态问题。但是演绎验证的过程一般为定理证明器辅助，人工参与，无法做到完全自动化，推导过程复杂，工作量大，效率低，不能适用于大型的复杂系统，因而适用范围较窄。常见的演绎验证工具有HOL，ACL2，PVS和TLV等。模型检测主要应用于验证并发的状态转换系统，通过遍历系统的状态空间，对有限状态系统进行全自动验证，快速高效地验证出系统是否满足其设计期望。下面将主要介绍模型检测方法的发展历史和研究现状，以及当前面临的挑战和未来发展方向等问题。　　2　模型检测及相关技

3、术　　模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式Φ。检测系统模型是否满足时态逻辑公式Φ，如果满足则返回是，不满足则返回否及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear　TemporalLogic)和计算树逻辑CTL(putation　Tree　Logic)。　　2.1　线性时态逻辑　　对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基

4、本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：∧(与)，∨(或)，

5、(非)，→(逻辑包含)，←→(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-tim

6、e)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M中是否存在从某个状态出发的并满足LTL公式

7、Φ的路径，如果所有路径都满足LTL公式Φ则不存在有路径满足

8、Φ。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。　　2.2　计算树逻辑　　计算树即为通过将迁移系统M某一状态作为根，将M用树形结构展开表示出来，CTL使用路径量词(包括：A(All)，E(Exist))和时态算子(包括F，G，X，U)对计算树属性进行形式化的描述，表示出系统的

9、状态变化以及状态的分枝情况。LTL的时间定义是与路径相关的，每个时刻只有唯一的一个后继状态。LTL可用于有重点的选择感兴趣的路径分析，并且LTL可以表达公平概念而CTL不能。但是对于一些复杂属性，如每个计算总是可能返回到初始状态，LTL将无法描述，但是CTL可以。CTL的时间定义是与状态相关的，每个状态都有多个可能的后继状态，从一个给定的状态量化分离出路径，能够断言行为的存在。CTL可以用路径量词E，而LTL不可以;CTL公式使用路径量词A时与LTL公式表达内容可以相同。LTL和CTL各有优势，Emerson等人提出扩展的时间逻辑CTL，提供了一种统一的框架，包含了L

10、TL和CTL，但是可满足性判定代价较高。　　2.3　模型检测工具　　模型检测因其自动化、高效等特点得到广泛应用，各类模型检测工具也层出不穷。以下是几类典型的模型检测工具。SPIN是1980年美国贝尔实验室开发的模型检测工具，主要关心系统进程间的交互问题。它以promela为建模语言，以LTL为系统属性的逻辑描述语言，支持on-the-fly技术，可以根据用户的需要生成系统的部分状态，而无需构建完整的状态迁移图。SPIN验证器无法验证实时系统。NuSMV是1987年由McMillan提出的开源的符号模型检测工具。它可以工作于批处理模式，也可以工作于交互