基于偏序规约技术的网络程序JPF验证

摘要

为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案.针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案.该方案通过消除线程启动时产生的冗余路径,有效减少了检测过程中产生的状态空间.实验结果表明,该方案能够有效消除对冗余状态的检测,减少了JPF对网络程序进行模型检测时产生的状态数.