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

Verification of networked programs based on partial order reduction using JPF

作　　者：杨翰文[1] 龙士工[1] 谢光颖 

机构地区：[1]贵州大学计算机科学与技术学院,贵州贵阳550025

出　　处：《计算机工程与设计》2014年第6期2004-2008,共5页Computer Engineering and Design

基　　金：国家自然科学基金项目(61163001)

摘　　要：为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案。针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案。该方案通过消除线程启动时产生的冗余路径,有效减少了检测过程中产生的状态空间。实验结果表明,该方案能够有效消除对冗余状态的检测,减少了JPF对网络程序进行模型检测时产生的状态数。To reduce the number of system states generated in the model checking process of networked programs,an architecture-aware partial order reduction solution was proposed.Aiming at solving the problem that the built-in partial order reduction mechanism of JPF model checker could not recognize the redundant states caused at the spawning of threads,a solution that could be applied in the model checking of networked program was designed.It could effectively decrease the state space generated during the checking process through eliminating the redundant paths produced at the spawning of threads.According to the results of experiment,this solution could effectively eliminate the checking of redundant state,and reduce the number of states produced during the model checking for networked programs using JPF.

关 键 词：模型检测 状态爆炸 偏序规约 on-the-fly技术 程序验证 

分 类 号：TP311.56[自动化与计算机技术—计算机软件与理论]