论文部分内容阅读
模型检验是对程序或系统使用严格的模型方法证明程序是否满足给定的性质。软件模型检验技术使用谓词抽象的自动化方法解决了整数、实数、循环边界等程序问题，但是对于中断冲突、资源竞争等系统问题并没有解决。而且由于软件资源竞争具有不确定性和难以重现的特点，对它的检测和调试也一直是一大难题。 首先，本文通过对资源竞争的原因及状态进行分析，提出使用运行时序检测与锁检测相结合的方法，从源语言中对软件资源竞争的内容进行特征提取，构造出能够识别资源竞争的布尔程序。然后，基于CPN和Promela分别对上述方法进行系统仿真和模型检验，从而验证提出的资源竞争检测方法的有效性，并得出两种模型在进行模型检验时各自的优缺点。最后，通过对实测系统使用模型检验方法测试，从而对本文提出的软件资源竞争的模型验证理论进行有效的验证。 本文的主要研究内容和创新点如下: 1、对源程序进行谓词抽象，将与资源竞争相关的内容进行特征提取，构造出能够识别竞争关系的布尔程序。直接对资源竞争进行谓词抽象，是本文的一个创新点。 2、本文将时序控制检测与锁检测相结合，构建出资源竞争检测模型，并使用模型检验方法进行系统仿真和模型检验，从而验证资源竞争检测的可行性。 3、根据不同任务调度策略的特点，以资源竞争检测为出发点，归纳总结出四种基于任务调度的资源竞争模型检测方法。 4、解决了软件模型检验中的一个难题，即设计出能够对资源竞争，尤其是中断冲突进行检测的软件模型检验方法。这是本文最重要的创新点。 5、在模型检验方法中分别使用CPN模型和Promela模型进行验证。 本文对基于CPN的资源竞争检测模型、基于Promela的资源竞争检测模型，以及基于任务调度的资源竞争模型检测方法，分别进行了理论证明、系统仿真和模型检验。实验结果表明本文提出的资源竞争检测方法是有效的、可靠的，可以为资源竞争自动检测系统的构建提供了相关的理论基础及技术支持。