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

Application of Program Slicing Technology to Concurrent Programming Model Checking

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

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.