基于嵌套树模型检测的研究

Research on model checking based on nested trees

文章针对软件验证过程中的结构抽象表示问题,考虑到结构程序的顺序结构、调用返回关系,给出了嵌套树以及嵌套状态机的定义。在该数据结构及μ演算的基础上,定义了嵌套树的μ演算(NT-μ)。NT-μ的公式语法是基于概要的,在嵌套状态机上提出基于概要类的模型检测。嵌套状态机的结点是有限的,且嵌套状态机有限的概要类对应于嵌套树中的无限的概要,因此该方法能提高检测的效率。

To solve the problems of structure abstract representation in the software verification process,taking into account the program sequence structure and the relationship between call and return,the definition of nested trees and nested state machine is given.Based on the data structure andμ-calculus,theμ-calculus of nested trees（NT-μ）is defined.The formula syntax of NT-μis based on the summary,and the model checking of summary class is presented.For the reason that the nodes in the nested state machine are finite,and the finite summary class in the nested state machine corresponds to the infinite summary in the nested tree,the method can improve the detection efficiency.