發(fā)布時(shí)間：2021-10-13 13:56

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

【文章來(lái)源】：南京大學(xué)江蘇省 211工程院校 985工程院校 教育部直屬院校

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

【學(xué)位級(jí)別】：碩士

【部分圖文】：

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

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

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

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

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



本文編號(hào)：3434802