软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2008年
1期
27-38
,共12页
屈婉霞%李暾%郭阳%杨晓东
屈婉霞%李暾%郭暘%楊曉東
굴완하%리돈%곽양%양효동
模型检验%谓词抽象%抽象求精%反例%插值
模型檢驗%謂詞抽象%抽象求精%反例%插值
모형검험%위사추상%추상구정%반례%삽치
随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.
隨著軟、硬件繫統規模和功能的不斷擴充,狀態空間爆炸問題嚴重影響瞭模型檢驗的進一步髮展與應用,成為驗證大規模繫統的瓶頸.謂詞抽象是解決狀態空間爆炸的最有效方法之一,近年來得到迅速髮展.介紹瞭謂詞抽象的基本算法併比較瞭不同的求解支持工具;重點分析瞭反例指導的抽象求精和基于插值的抽象求精原理;分析瞭產生新謂詞的各種方法的優、缺點;最後指齣瞭謂詞抽象技術進一步髮展所麵臨的挑戰和髮展方嚮.
수착연、경건계통규모화공능적불단확충,상태공간폭작문제엄중영향료모형검험적진일보발전여응용,성위험증대규모계통적병경.위사추상시해결상태공간폭작적최유효방법지일,근년래득도신속발전.개소료위사추상적기본산법병비교료불동적구해지지공구;중점분석료반례지도적추상구정화기우삽치적추상구정원리;분석료산생신위사적각충방법적우、결점;최후지출료위사추상기술진일보발전소면림적도전화발전방향.
