信息物理系統(tǒng)廣泛應用于安全攸關(guān)領(lǐng)域,因此要保證其正確性與安全性至關(guān)重要。混成自動機是一種既包含了離散的狀態(tài)轉(zhuǎn)移,又存在連續(xù)變量變化的形式化建模語言。其中離散的邏輯跳轉(zhuǎn)與連續(xù)的變量變化混合的特性使得其可以用于對信息物理系統(tǒng)建模與驗證。然而正因為離散跳轉(zhuǎn)與連續(xù)行為的交織,使得其狀態(tài)空間極為復雜,即便是對混成自動機安全性問題的可達性問題的驗證也異常困難。在實際的信息物理系統(tǒng)中,由于不同組件通信協(xié)作行為的大量存在,組合混成自動機才能滿足其建模需求。組合混成自動機由多個單一混成自動機通過同步行為協(xié)作構(gòu)成,其行為比單一混成自動機更為復雜。目前的研究工作能解決的組合混成自動機驗證問題的規(guī)模極為有限。因此如何提高組合混成自動機可達性驗證規(guī)模,提升驗證效率是十分值得關(guān)注與研究的課題。本文針對組合混成自動機的子類——組合線性混成自動機的可達性驗證進行了系統(tǒng)化研究,研究內(nèi)容包括:1.基于混合語義的組合線性混成自動機有界可達性驗證。本文工作提出了一種基于混合語義的組合線性混成自動機有界可達性驗證方法。該方法采用傳統(tǒng)交替語義枚舉候選路徑,淺同步語義驗證路徑行為。通過將組合自動機的離散圖結(jié)構(gòu)編碼為SAT問題的方式... 

【文章來源】：南京大學江蘇省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：79 頁

【學位級別】：碩士

【部分圖文】：

圖４－８：?ＦＤＤ［實驗數(shù)據(jù)??

在?ＦＤＤ丨和?Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ?的不可達版本中，ＢＡＣＨ－ｓｔｅｐ?與?ＢＡＣＨ－??ｍｕｌｔｉｐｌｅ?能處?理的問?題?規(guī)模相?Ｍ?。?ｆｒ：?ＦＤ［）Ｉ?模型上?ｍｕｌｔｉｐｌｅ?幣體?能在?更短的??時間內(nèi)完成驗證，原因在于精確定位的１ＩＳ能幫助約減吏多的路徑，節(jié)約驗證??時間。在Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ上驗證時間基本持平，分析發(fā)現(xiàn)，該模型在圖結(jié)構(gòu)??

在?ＦＤＤ丨和?Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ?的不可達版本中，ＢＡＣＨ－ｓｔｅｐ?與?ＢＡＣＨ－??ｍｕｌｔｉｐｌｅ?能處?理的問?題?規(guī)模相?Ｍ?。?ｆｒ：?ＦＤ［）Ｉ?模型上?ｍｕｌｔｉｐｌｅ?幣體?能在?更短的??時間內(nèi)完成驗證，原因在于精確定位的１ＩＳ能幫助約減吏多的路徑，節(jié)約驗證??時間。在Ｒｉｎｇ－Ｓｈａｐｅ?Ｆｉｓｃｈｅｒ上驗證時間基本持平，分析發(fā)現(xiàn)，該模型在圖結(jié)構(gòu)??

【參考文獻】：
期刊論文
[1]基于組合IIS路徑抽取的組合線性混成系統(tǒng)有界可達性分析優(yōu)化[J]. 解定寶,周岳翔,卜磊,王林章,李宣東.  中國科學:信息科學. 2017(03)
[2]混成系統(tǒng)形式化驗證[J]. 卜磊,解定寶.  軟件學報. 2014(02)

博士論文
[1]混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究[D]. 解定寶.南京大學 2016



本文編號：3434802