供熱混合系統(tǒng)的抽象及其形式化驗(yàn)證.pdf

1、本文采用了兩者結(jié)合的方法，先對(duì)供熱混合系統(tǒng)用基于定性推理的方法，將其轉(zhuǎn)變?yōu)殡x散的抽象系統(tǒng)，并用Matlab中的圖形化建模工具Stateflow建立了離散狀態(tài)模型圖，再采用符號(hào)模型驗(yàn)證工具SMV(Symbolic Model Verification)進(jìn)行自動(dòng)驗(yàn)證。 針對(duì)供熱混合系統(tǒng)形式化驗(yàn)證中狀態(tài)空間爆炸問題，本文利用在定性推理的方法上進(jìn)行擴(kuò)展，基于實(shí)數(shù)域求n階導(dǎo)數(shù)進(jìn)行數(shù)據(jù)抽象，將復(fù)雜的混合系統(tǒng)，簡化為抽象離散系統(tǒng)，不但有效地降低系統(tǒng)

2、復(fù)雜程度，簡化后的系統(tǒng)更容易被分析，而且仍然充分地保留了系統(tǒng)的安全特性。 此外，本文利用符號(hào)模型驗(yàn)證工具SMV對(duì)供熱系統(tǒng)抽象后的離散模型實(shí)現(xiàn)了自動(dòng)驗(yàn)證。SMV基于OBDDs的搜索算法確定系統(tǒng)是否滿足用計(jì)算樹邏輯CTL描述的被驗(yàn)證性質(zhì)。符號(hào)化表示對(duì)于數(shù)字電路設(shè)計(jì)的建模十分自然,而且能夠驗(yàn)證具有極大狀態(tài)空間的系統(tǒng)。由于混合系統(tǒng)驗(yàn)證的重點(diǎn)是狀態(tài)空間的劃分，故在文章的最后對(duì)其它幾種混合系統(tǒng)的形式化驗(yàn)證方法做了比較。同其它方法相比，本文計(jì)算抽