检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
机构地区:[1]上海大学计算机工程与科学学院,上海200072
出 处:《计算机技术与发展》2008年第11期163-167,171,共6页Computer Technology and Development
摘 要:模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则,并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。Despite the success of model checking for hardware and protocol design, there are many difficulties in software model checking. The main problem is automatic extraction of models from codes and how to reduce the state space of the model extracted from codes. An application of program dicing to handle the issues mentioned above is presented, which include how to map the specification used in model checking to the slicing rule and how to transfer the slices of the program to the model for checking. The resulte is that it is an efficient way to improve .software model checking.
关 键 词:并发程序 模型检查 程序切片 状态空间 切片准则
分 类 号:TP301.2[自动化与计算机技术—计算机系统结构]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.116