计算机辅助设计与图形学学报
計算機輔助設計與圖形學學報
계산궤보조설계여도형학학보
JOURNAL OF COMPUTER-AIDED DESIGN & COMPUTER GRAPHICS
2014年
6期
991-998
,共8页
张龙%屈婉霞%郭阳%李思昆
張龍%屈婉霞%郭暘%李思昆
장룡%굴완하%곽양%리사곤
参数化系统%模型检验%二维抽象%有限状态机
參數化繫統%模型檢驗%二維抽象%有限狀態機
삼수화계통%모형검험%이유추상%유한상태궤
parameterized systems%model checking%two-dimensional abstraction%finite state machine
针对参数化系统验证面临的状态空间爆炸问题,提出自动抽象方法化简参数化系统状态空间.首先进行y-抽象建立单进程有限状态机模型,然后通过对多个y-抽象模型的合成运算得到异步合成的参数化系统,最后根据定义的谓词对参数化系统进行X-抽象得到二维抽象模型.运用该方法,对基于Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7个参数化协议和注入错误的MESI协议进行自动化抽象建模,并验证了相关性质,有效地提升了验证参数化系统的能力、缩短了验证时间;应用文中方法验证FT-1000 CPU的一致性协议的结果表明,该方法在降低验证复杂度方面具有明显优势.
針對參數化繫統驗證麵臨的狀態空間爆炸問題,提齣自動抽象方法化簡參數化繫統狀態空間.首先進行y-抽象建立單進程有限狀態機模型,然後通過對多箇y-抽象模型的閤成運算得到異步閤成的參數化繫統,最後根據定義的謂詞對參數化繫統進行X-抽象得到二維抽象模型.運用該方法,對基于Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly和Dragon的7箇參數化協議和註入錯誤的MESI協議進行自動化抽象建模,併驗證瞭相關性質,有效地提升瞭驗證參數化繫統的能力、縮短瞭驗證時間;應用文中方法驗證FT-1000 CPU的一緻性協議的結果錶明,該方法在降低驗證複雜度方麵具有明顯優勢.
침대삼수화계통험증면림적상태공간폭작문제,제출자동추상방법화간삼수화계통상태공간.수선진행y-추상건립단진정유한상태궤모형,연후통과대다개y-추상모형적합성운산득도이보합성적삼수화계통,최후근거정의적위사대삼수화계통진행X-추상득도이유추상모형.운용해방법,대기우Synapse N+1,Illinois,MESI,MOESI,Berkeley,Firefly화Dragon적7개삼수화협의화주입착오적MESI협의진행자동화추상건모,병험증료상관성질,유효지제승료험증삼수화계통적능력、축단료험증시간;응용문중방법험증FT-1000 CPU적일치성협의적결과표명,해방법재강저험증복잡도방면구유명현우세.
