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

Application of Program Slicing Technology to Concurrent Programming Model Checking

作　　者：高鹏飞[1] 沈云付[1] 

机构地区：[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[自动化与计算机技术—计算机系统结构]