[1]高鹏飞 沈云付.程序切片技术在并发程序模型检查中的应用[J].计算机技术与发展,2008,(11):163-167.
GAO Peng-fei,SHEN Yun-fu.Application of Program Slicing Technology to Concurrent Programming Model Checking[J].,2008,(11):163-167.
点击复制
程序切片技术在并发程序模型检查中的应用(
)
《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]
- 卷:
-
- 期数:
-
2008年11期
- 页码:
-
163-167
- 栏目:
-
应用开发研究
- 出版日期:
-
1900-01-01
文章信息/Info
- Title:
-
Application of Program Slicing Technology to Concurrent Programming Model Checking
- 文章编号:
-
1673-629X（2008）11-0163-05
- 作者:
-
高鹏飞 沈云付
-
上海大学计算机工程与科学学院
- Author(s):
-
GAO Peng-fei; SHEN Yun-fu
-
SCh. of Computer Engineering and Science, Shanghai University
-
- 关键词:
-
并发程序; 模型检查; 程序切片; 状态空间; 切片准则
- Keywords:
-
concurrent programming; software model checking; program slicing; state space; slicing criterion
- 分类号:
-
TP301.2
- 文献标志码:
-
A
- 摘要:
-
模型检查技术在硬件和协议设计方面已经取得很大成功，但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究，来解决并发程序验证的建模问题，包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后，软件模型检查效率得到提高
- Abstract:
-
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 cod
备注/Memo
- 备注/Memo:
-
高鹏飞（1980-），女，内蒙古人，硕士研究生，研究方向为形式化验证、模型检查；沈云付，博士，副教授，研究方向为形式化方法、高性能并行计算
更新日期/Last Update:
1900-01-01