【摘要】：多值模型可用于對包含不確定與不一致信息的軟件系統(tǒng)進(jìn)行建模與驗(yàn)證。提出了采用基于分解的方式來刻畫多值模型之間的逼近關(guān)系,這為采用抽象方法解決模型檢測時(shí)所產(chǎn)生的狀態(tài)爆炸問題奠定了理論基礎(chǔ)。為此,首先給出了多值模型分解為多個(gè)三值模型的方法,并且證明了任意μ演算公式在多值模型上的檢測結(jié)果等于在分解后所有三值模型上的檢測結(jié)果的合并。進(jìn)一步,由三值模型上的混合模擬關(guān)系給出了多值模型間逼近關(guān)系的結(jié)構(gòu)定義,并證明對于任意給定的兩個(gè)滿足逼近關(guān)系的多值模型,μ演算公式在其上的檢測結(jié)果在信息序關(guān)系上得以保持。
[Abstract]:Multi-valued model can be used to model and verify software systems with uncertain and inconsistent information. In this paper, a decomposition-based approach is proposed to depict the approximate relationship between multivalued models, which lays a theoretical foundation for solving the state explosion problem caused by model detection by abstract method. In this paper, the method of decomposing the multi-valued model into multiple ternary models is given, and it is proved that the detection results of any 渭 calculus formula on the multi-valued model are equal to the combination of the detection results on all the ternary models after decomposition. Furthermore, the structure definition of the approximation relation between the multivalued models is given from the mixed simulation relation on the ternary model, and it is proved that for any given two multivalued models satisfying the approximation relation, the detection results of the 渭 formula can be maintained in the information order relation.
【作者單位】： 南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;
【基金】：國家自然科學(xué)基金項(xiàng)目(61170043,61100034)資助
【分類號】：TP306

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 魏歐;袁泳;蔡昕燁;黃志球;徐丙鳳1;;循環(huán)對稱化簡及在三值模型上的擴(kuò)展[J];軟件學(xué)報(bào);2011年06期

【共引文獻(xiàn)】

相關(guān)期刊論文 前1條

1 陳娟娟;魏歐;黃志球;陳哲;;基于雙格的多值模型的精化關(guān)系與對稱化簡[J];計(jì)算機(jī)工程與應(yīng)用;2013年22期

【二級參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 蒲飛;張文輝;;結(jié)合搜索空間劃分和抽象進(jìn)行LTL模型檢測[J];中國科學(xué)(E輯:信息科學(xué));2007年12期

，

本文編號：2499298