本文關鍵詞：ProMiner:系統(tǒng)性質(zhì)驅動的雙向一致性檢驗框架

  更多相關文章： 一致性檢驗 模型檢測 基于模型的測試 線性時序邏輯

【摘要】：在模型驅動軟件開發(fā)過程中,基于模型的測試方法往往用于檢驗軟件代碼針對軟件模型的一致性以確保軟件質(zhì)量.然而,隨著當今軟件系統(tǒng)規(guī)模的不斷擴大,相應的軟件開發(fā)過程也變得越來越靈活,代碼有時會先于模型被修改,以更忠實地體現(xiàn)系統(tǒng)功能和實現(xiàn)機制.傳統(tǒng)的基于模型的測試方法只能檢測代碼之于模型的一致性而不能反作用于模型層面,模型的修改者只能人為地評估修改的正確性,大大降低了效率并增加了系統(tǒng)的潛在隱患.為此,對傳統(tǒng)基于模型的測試方法的一致性檢驗進行了擴展,實現(xiàn)了一致性檢驗框架Pro Miner,通過抽取表達模型與代碼的不一致的系統(tǒng)性質(zhì)來自動定位模型中與實際運行系統(tǒng)不匹配的部分,并將其表示為可直接用于模型檢測的線性時序邏輯(LTL)表達式,以支持軟件模型和代碼間雙向的一致性檢驗.實驗結果表明,Pro Miner可有效查找軟件模型和代碼間的不一致并生成可直接檢測模型的系統(tǒng)性質(zhì),從而實現(xiàn)了自動化的模型與代碼間的雙向一致性檢測,不僅提高了一致性檢測的有效性,而且大大減少了人力開銷.
【作者單位】： 華東師范大學計算機科學技術系;上海市高可信計算重點實驗室(華東師范大學);
【關鍵詞】： 一致性檢驗 模型檢測 基于模型的測試 線性時序邏輯
【基金】：上海市自然科學基金(13ZR1413000) 核高基重大專項(2014ZX01038-101-001) 國家自然科學基金(61502170,91118008) 國家基金委國際合作項目(中丹)(61361136002);國家基金委創(chuàng)新研究群體項目(61321064)~~
【分類號】：TP311.52
【正文快照】：

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前8條

1 章s，

本文編號：909115