程序切片技术在并发程序模型检查中的应用

• 作者: 沈云付 高鹏飞
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 并发程序 模型检查 程序切片 状态空间 切片准则
• 年，卷（期）: 2008,（11）
• 所属期刊栏目: 应用开发研究
• 页码范围: 163-167,171
• 页数: 6页
• 分类号: TP301.2
• 字数: 5166字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2008.11.047

摘要

模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难.其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间.文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则,并把得到的程序切片转化为验证所需的模型.经程序切片处理后,软件模型检查效率得到提高.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	沈云付	上海大学计算机工程与科学学院	31	119	7.0	10.0
2	高鹏飞	上海大学计算机工程与科学学院	2	4	1.0	2.0