The finite-state model checking of software is still limited by the notorious state-explosion problem. The dependence-based program slicing is effective to reduce the verification time and is orthogonal to other reduction techniques of model checking. However, within slicing concurrent programs for model checking, the conversions between multiple irreplaceable models and the calculation of dependencies for some variables irrelevant to the verified property produce redundant calculating costs. Thus, we propose a Program Dependence Net (PDNet) as a unified model combining the control-flow structure with dependencies to avoid the model conversions. For reduction, we propose a PDNet slicing to capture the relevant variables' dependencies on demand. The calculating costs could be significantly compressed by our unified model and on-demand slicing based on PDNet. Then, we implemented a concurrent program model checking tool based on PDNet and its slice. Finally, we validated the advantages of our methods.
翻译:软件的有限状态模式检查仍然受到臭名昭著的状态爆炸问题的限制。 基于依赖性的程序切片对于减少核查时间是有效的,并且与其他减少模型检查技术是正反的。然而,在同时切片的模型检查程序内部,多个不可替代的模式之间的转换以及与核实的属性无关的某些变量的依附性计算产生了多余的计算成本。因此,我们提议一个程序依赖性网络(PDNet)作为将控制流结构与依赖性相结合的统一模式,以避免模型转换。为了减少,我们建议使用一个PD网络切片,我们建议使用一个PDNet切片来捕捉相关变量对需求的依赖性。计算成本可以通过我们基于PDNet的统一模型和按需切片的切片进行大幅压缩。然后,我们采用了一个基于PDNet及其切片的并行程序模式检查工具。最后,我们验证了我们方法的优点。