电子与信息学报
電子與信息學報
전자여신식학보
JOURNAL OF ELECTRONICS & INFORMATION TECHNOLOGY
2011年
4期
902-907
,共6页
李兴锋%张新常%杨美红%阎保平
李興鋒%張新常%楊美紅%閻保平
리흥봉%장신상%양미홍%염보평
模型检测%扩展有限状态自动机%状态爆炸
模型檢測%擴展有限狀態自動機%狀態爆炸
모형검측%확전유한상태자동궤%상태폭작
该文针对模型检测过程中所存在的状态爆炸问题,提出了一种基于模型检测工具SPIN的模块化模型检测方法.所提出的方法能够将指定的抽象模型分解成若干的模块,并对这些验证复杂度相对低的模块执行模型检测,以替代对原模型的模型检测.所提方法所用的分解过程保留了原模型所有的语义,同时不增加额外的语义,从而使得验证所有模块等同于验证原模型.理论和实验分析结果显示了所提方法的有效性.
該文針對模型檢測過程中所存在的狀態爆炸問題,提齣瞭一種基于模型檢測工具SPIN的模塊化模型檢測方法.所提齣的方法能夠將指定的抽象模型分解成若榦的模塊,併對這些驗證複雜度相對低的模塊執行模型檢測,以替代對原模型的模型檢測.所提方法所用的分解過程保留瞭原模型所有的語義,同時不增加額外的語義,從而使得驗證所有模塊等同于驗證原模型.理論和實驗分析結果顯示瞭所提方法的有效性.
해문침대모형검측과정중소존재적상태폭작문제,제출료일충기우모형검측공구SPIN적모괴화모형검측방법.소제출적방법능구장지정적추상모형분해성약간적모괴,병대저사험증복잡도상대저적모괴집행모형검측,이체대대원모형적모형검측.소제방법소용적분해과정보류료원모형소유적어의,동시불증가액외적어의,종이사득험증소유모괴등동우험증원모형.이론화실험분석결과현시료소제방법적유효성.
