首页 | 本学科首页   官方微博 | 高级检索  
     检索      

基于嵌套树模型检测的研究
引用本文:郭婧,徐中伟,李丽梅.基于嵌套树模型检测的研究[J].合肥工业大学学报(自然科学版),2015(4).
作者姓名:郭婧  徐中伟  李丽梅
作者单位:1. 同济大学 电子与信息工程学院,上海,201804
2. 九江学院 图书馆,江西 九江,332005
基金项目:国家自然科学基金资助项目(61075002);国家科技支撑计划重大资助项目
摘    要:文章针对软件验证过程中的结构抽象表示问题,考虑到结构程序的顺序结构、调用返回关系,给出了嵌套树以及嵌套状态机的定义。在该数据结构及μ演算的基础上,定义了嵌套树的μ演算(NT-μ)。NT-μ的公式语法是基于概要的,在嵌套状态机上提出基于概要类的模型检测。嵌套状态机的结点是有限的,且嵌套状态机有限的概要类对应于嵌套树中的无限的概要,因此该方法能提高检测的效率。

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

Research on model checking based on nested trees
GUO Jing,XU Zhong-wei,LI Li-mei.Research on model checking based on nested trees[J].Journal of Hefei University of Technology(Natural Science),2015(4).
Authors:GUO Jing  XU Zhong-wei  LI Li-mei
Abstract:
Keywords:model checking  nested tree  nested state machine  μ-calculus  software verification
本文献已被 CNKI 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号