隨著科技的進(jìn)步,尤其是電子技術(shù)的長(zhǎng)足發(fā)展,以及社會(huì)生產(chǎn)和生活的需求,計(jì)算機(jī)相關(guān)的技術(shù)對(duì)各種技術(shù)領(lǐng)域的涉及程度越來(lái)越廣泛和深入,這就導(dǎo)致了以連續(xù)與離散行為共存為特點(diǎn)的混合系統(tǒng)的廣泛使用。我們從形式化地角度來(lái)研究混合系統(tǒng)。目前混合系統(tǒng)的形式化分析、驗(yàn)證與模擬方法主要有兩類(lèi),即演算推演法和混合自動(dòng)機(jī)法,二者的理論都已經(jīng)比較成熟,都要求將實(shí)例空間映射到理論空間,而后應(yīng)用這些成熟的理論和方法進(jìn)行分析驗(yàn)證。但是上述兩個(gè)空間的映射,即建模方法,目前還比較混亂,并沒(méi)有形成統(tǒng)一的有效框架,還處于具體實(shí)例具體分析的手工階段。 混合系統(tǒng)的研究對(duì)象包含控制系統(tǒng)、嵌入式系統(tǒng)和Cyber Physical系統(tǒng)等,這些系統(tǒng)的設(shè)計(jì)階段都大量采用了成熟的層次化設(shè)計(jì)思路,并生成大量的層次化設(shè)計(jì)文檔。那么快速準(zhǔn)確地從層次化設(shè)計(jì)中得到混合系統(tǒng)形式化分析模型,并對(duì)此模型進(jìn)行分析驗(yàn)證的工作就非常具有實(shí)際意義。 本文研究將這種工業(yè)界常用的層次化設(shè)計(jì),直接對(duì)應(yīng)到混合系統(tǒng)形式化分析對(duì)象的方法。我們的依據(jù)是一種廣泛采用的層次化設(shè)計(jì)概念模型[24],首先研究這種層次化概念模型的符號(hào)化表示,即層次化形式模型,而后基于此形式模型,探討時(shí)段演算推演方法及混合自動(dòng)機(jī)方法的語(yǔ)義,將此層次化混合系統(tǒng)形式模型映射為時(shí)段公式或混合自動(dòng)機(jī),最后按照(擴(kuò)展)時(shí)段演算和混合自動(dòng)機(jī)理論進(jìn)行分析驗(yàn)證,并給出實(shí)例來(lái)闡述這種方法的可行性。
【學(xué)位單位】：蘭州大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位年份】：2011
【中圖分類(lèi)】：O242.1;N94
【部分圖文】：

基于層次模型的混合系統(tǒng)形式化分析與個(gè)復(fù)雜的大問(wèn)題變成許多簡(jiǎn)單的小問(wèn)題，而且形式化的層次模型可混合系統(tǒng)的時(shí)間驅(qū)動(dòng)和事件驅(qū)動(dòng)行為。這種層次化分析方法是一種如著名的因特網(wǎng)051模型)，適用性強(qiáng)，分析步驟簡(jiǎn)單清晰的方法，非際問(wèn)題的快速刻畫(huà)。層次化方法己經(jīng)是工業(yè)界廣泛采用的設(shè)計(jì)方法，合系統(tǒng)設(shè)計(jì)都采用或者可以通過(guò)簡(jiǎn)單變換而對(duì)應(yīng)到這種方法。過(guò)對(duì)國(guó)內(nèi)外同行相關(guān)文獻(xiàn)的研讀和相關(guān)工作的追蹤，和對(duì)目前可見(jiàn)系統(tǒng)建模方法的比較，我們選取圖3.2中的層次化建模方法作為我們，并稱(chēng)圖中所示的層次化建模方法為混合系統(tǒng)的層次化概念模型，型列出了一條完整地分層描述混合系統(tǒng)的途徑。

圖4.2:時(shí)間軸上的棍合系統(tǒng)層次化概念模型「加、〕表示時(shí)間段上每一個(gè)時(shí)間點(diǎn)都為真的斷言，即描述全狀「尸魂等價(jià)于了尸一乙由于時(shí)間點(diǎn)上的斷一言成立.與否不會(huì)影響時(shí)段演算的結(jié)果，所以不將這種斷盲一單獨(dú)列出，僅僅用「1來(lái)表示，依據(jù)推演時(shí)的上下問(wèn)點(diǎn)斷一言。這里我們也不考慮這種斷一言的語(yǔ)義。最后，量化的斷言口尸和令尸分別表示混合系統(tǒng)‘最終”和“總是”，其語(yǔ)義如下:I江口p衛(wèi)【乙，e{全V乙，e任!O，co」:11今p衛(wèi)【乙，。」全日乙，e任【O，oo」:三。.1江p衛(wèi)【白，e」三。一I江p衛(wèi)【吞，e」4.3.1基于混合系統(tǒng)層次化形式模型的證明體系

圖4.3:比例積分智能控制時(shí)水位隨時(shí)間的曲線(xiàn)使用擴(kuò)展時(shí)段演算推演程控水箱系統(tǒng)4.1可知，系統(tǒng)設(shè)計(jì)凡咖，5在所有時(shí)段上都為真，即「凡咖們來(lái)證明三條安全性性質(zhì):「凡vbs川井口「0三h。三H八。:t司

【參考文獻(xiàn)】

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

1 李曉山，周巢塵;時(shí)段演算綜述[J];計(jì)算機(jī)學(xué)報(bào);1994年11期

本文編號(hào)：2811712