计算机与数字工程
計算機與數字工程
계산궤여수자공정
COMPUTER & DIGITAL ENGINEERING
2006年
2期
93-96
,共4页
模型检测%软件测试%强制性逻辑关系%状态爆炸
模型檢測%軟件測試%彊製性邏輯關繫%狀態爆炸
모형검측%연건측시%강제성라집관계%상태폭작
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题.在为此提出的诸多理论和方法中,模型检测(model checking)以其简洁明了和自动化程度高而引人注目.具体介绍了模型检测的一些理论,同时将它应用于具体的软件程序,运用模型检测方法对软件进行测试.从而证明了模型检测方法与测试结合对于软件可靠性和正确性所起的巨大作用.
隨著計算機軟硬件繫統日益複雜,如何保證其正確性和可靠性成為日益緊迫的問題.在為此提齣的諸多理論和方法中,模型檢測(model checking)以其簡潔明瞭和自動化程度高而引人註目.具體介紹瞭模型檢測的一些理論,同時將它應用于具體的軟件程序,運用模型檢測方法對軟件進行測試.從而證明瞭模型檢測方法與測試結閤對于軟件可靠性和正確性所起的巨大作用.
수착계산궤연경건계통일익복잡,여하보증기정학성화가고성성위일익긴박적문제.재위차제출적제다이론화방법중,모형검측(model checking)이기간길명료화자동화정도고이인인주목.구체개소료모형검측적일사이론,동시장타응용우구체적연건정서,운용모형검측방법대연건진행측시.종이증명료모형검측방법여측시결합대우연건가고성화정학성소기적거대작용.