国防科技大学学报
國防科技大學學報
국방과기대학학보
JOURNAL OF NATIONAL UNIVERSITY OF DEFENSE TECHNOLOGY
2008年
4期
53-58
,共6页
屈婉霞%李暾%郭阳%杨晓东
屈婉霞%李暾%郭暘%楊曉東
굴완하%리돈%곽양%양효동
模型检验%显式状态枚举%可达性分析
模型檢驗%顯式狀態枚舉%可達性分析
모형검험%현식상태매거%가체성분석
随着软硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.在显式模型检验工具Murphi的基础上,针对其可达状态空间组织存在的问题进行改进,提出了基于整型指针与Fibonacci散列的可达状态空间组织方法,实现了一个高效的显式模型检验原型系统,在确保验证正确的同时有效缩短了验证时间,并能在系统规范不可满足的情况下给出反例,有助于系统设计人员快速定位错误.理论分析和实验结果表明了本方法的有效性.
隨著軟硬件繫統規模和功能的不斷擴充,狀態空間爆炸問題嚴重影響瞭模型檢驗的進一步髮展與應用,成為驗證大規模繫統的瓶頸.在顯式模型檢驗工具Murphi的基礎上,針對其可達狀態空間組織存在的問題進行改進,提齣瞭基于整型指針與Fibonacci散列的可達狀態空間組織方法,實現瞭一箇高效的顯式模型檢驗原型繫統,在確保驗證正確的同時有效縮短瞭驗證時間,併能在繫統規範不可滿足的情況下給齣反例,有助于繫統設計人員快速定位錯誤.理論分析和實驗結果錶明瞭本方法的有效性.
수착연경건계통규모화공능적불단확충,상태공간폭작문제엄중영향료모형검험적진일보발전여응용,성위험증대규모계통적병경.재현식모형검험공구Murphi적기출상,침대기가체상태공간조직존재적문제진행개진,제출료기우정형지침여Fibonacci산렬적가체상태공간조직방법,실현료일개고효적현식모형검험원형계통,재학보험증정학적동시유효축단료험증시간,병능재계통규범불가만족적정황하급출반례,유조우계통설계인원쾌속정위착오.이론분석화실험결과표명료본방법적유효성.
