模型检测技术在软件并行缺陷检测中的应用

Application of Model Checking Technology in Software Concurrent Defect Detection

多线程并行运行的软件在提高性能的同时,其交互的组合随着程序规模增大变得更为复杂,给软件的设计与验证带来了挑战。本文从常见的并行缺陷入手,提出使用模型检测的方法对其进行检测和分析,实践表明,使用该方法可有效检测此类并行缺陷。

Multithreading parallel running software not only improves the performance, but also brings challenges to software design and verification, because the combination of its interaction becomes more complex with the increase of program size. In this paper, the common concurrent defects are analyzed and verified by using model checking method. The practice shows that this method can effectively this kind of concurrent defects.