计算机工程与设计
計算機工程與設計
계산궤공정여설계
COMPUTER ENGINEERING AND DESIGN
2014年
6期
2004-2008
,共5页
模型检测%状态爆炸%偏序规约%on-the-fly技术%程序验证
模型檢測%狀態爆炸%偏序規約%on-the-fly技術%程序驗證
모형검측%상태폭작%편서규약%on-the-fly기술%정서험증
model checking%state explosion%partial order reduction (POR)%on-the-fly%program verification
为了减少网络程序模型检测过程中产生的系统状态数目,提出了一种架构感知偏序规约方案.针对目前模型检测器JPF内置的偏序规约机制不能够识别出线程启动时产生的冗余状态问题,设计了一种可应用于JPF的网络程序模型检测的解决方案.该方案通过消除线程启动时产生的冗余路径,有效减少了检测过程中产生的状态空间.实验结果表明,该方案能够有效消除对冗余状态的检测,减少了JPF对网络程序进行模型检测时产生的状态数.
為瞭減少網絡程序模型檢測過程中產生的繫統狀態數目,提齣瞭一種架構感知偏序規約方案.針對目前模型檢測器JPF內置的偏序規約機製不能夠識彆齣線程啟動時產生的冗餘狀態問題,設計瞭一種可應用于JPF的網絡程序模型檢測的解決方案.該方案通過消除線程啟動時產生的冗餘路徑,有效減少瞭檢測過程中產生的狀態空間.實驗結果錶明,該方案能夠有效消除對冗餘狀態的檢測,減少瞭JPF對網絡程序進行模型檢測時產生的狀態數.
위료감소망락정서모형검측과정중산생적계통상태수목,제출료일충가구감지편서규약방안.침대목전모형검측기JPF내치적편서규약궤제불능구식별출선정계동시산생적용여상태문제,설계료일충가응용우JPF적망락정서모형검측적해결방안.해방안통과소제선정계동시산생적용여로경,유효감소료검측과정중산생적상태공간.실험결과표명,해방안능구유효소제대용여상태적검측,감소료JPF대망락정서진행모형검측시산생적상태수.
