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

Research on model checking based on nested trees

作　　者：郭婧[1] 徐中伟[1] 李丽梅[2] 

机构地区：[1]同济大学电子与信息工程学院,上海201804 [2]九江学院图书馆,江西九江332005

出　　处：《合肥工业大学学报（自然科学版）》2015年第4期479-484,共6页Journal of Hefei University of Technology：Natural Science

基　　金：国家自然科学基金资助项目(61075002);国家科技支撑计划重大资助项目(2011BAG01B03)

摘　　要：文章针对软件验证过程中的结构抽象表示问题,考虑到结构程序的顺序结构、调用返回关系,给出了嵌套树以及嵌套状态机的定义。在该数据结构及μ演算的基础上,定义了嵌套树的μ演算(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.

关 键 词：模型检测 嵌套树 嵌套状态机 μ-演算 软件验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]