计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
7期
135-139,161
,共6页
模型验证%化简%抽象%状态爆炸
模型驗證%化簡%抽象%狀態爆炸
모형험증%화간%추상%상태폭작
Model verification%Reduction%Abstract%State space explosion
状态爆炸问题导致CP nets并发模型的正确性验证工作十分困难.提出了基于并发属性的模型化简方法和基于功能组合的模型抽象方法,用于对模型进行处理,移去与并发属性不相关的模型元素,提升模型的抽象层次,使模型状态空间规模得到显著降低,并在并发属性相关行为上与原模型保持一致;在处理后模型中运用状态空间分析、模型检测等验证方法完成模型验证,针对验证得出的模型错误,通过处理前后模型的对照关系在原模型中进行改正.这在一定程度上避免了状态爆炸问题并实现了模型验证.通过将上述方法应用于HMIPv6协议模型,验证了其有效性.
狀態爆炸問題導緻CP nets併髮模型的正確性驗證工作十分睏難.提齣瞭基于併髮屬性的模型化簡方法和基于功能組閤的模型抽象方法,用于對模型進行處理,移去與併髮屬性不相關的模型元素,提升模型的抽象層次,使模型狀態空間規模得到顯著降低,併在併髮屬性相關行為上與原模型保持一緻;在處理後模型中運用狀態空間分析、模型檢測等驗證方法完成模型驗證,針對驗證得齣的模型錯誤,通過處理前後模型的對照關繫在原模型中進行改正.這在一定程度上避免瞭狀態爆炸問題併實現瞭模型驗證.通過將上述方法應用于HMIPv6協議模型,驗證瞭其有效性.
상태폭작문제도치CP nets병발모형적정학성험증공작십분곤난.제출료기우병발속성적모형화간방법화기우공능조합적모형추상방법,용우대모형진행처리,이거여병발속성불상관적모형원소,제승모형적추상층차,사모형상태공간규모득도현저강저,병재병발속성상관행위상여원모형보지일치;재처리후모형중운용상태공간분석、모형검측등험증방법완성모형험증,침대험증득출적모형착오,통과처리전후모형적대조관계재원모형중진행개정.저재일정정도상피면료상태폭작문제병실현료모형험증.통과장상술방법응용우HMIPv6협의모형,험증료기유효성.
