實時系統(tǒng)是指能夠在指定或確定的時間內(nèi)完成事件處理的計算機應用系統(tǒng),其正確性不僅僅取決于其計算邏輯的正確性,并且與計算結(jié)果的產(chǎn)生時間有極大關系。在航空航天、生產(chǎn)控制、交通指揮、國防、核工業(yè)等安全攸關領域,實時系統(tǒng)發(fā)揮了至關重要的作用。因此保證實時系統(tǒng)的正確性和可靠性十分重要。模型檢測是一種自動化地驗證有限狀態(tài)系統(tǒng)的技術。上世紀90年代,模型檢測方法被應用到實時系統(tǒng)的可靠性和正確的檢測上。模型檢測針對的實時系統(tǒng)通常是封閉的,其運行結(jié)果只與系統(tǒng)自身的運行狀態(tài)有關。然而在實際生活中,實時系統(tǒng)往往會間接或直接地受到外界因素的影響。因此我們需要合成一個控制器使得在外界因素影響下,系統(tǒng)仍然滿足給定的性質(zhì),這就是控制器合成問題,它可以形式化的定義為:給定一個系統(tǒng)模型S和系統(tǒng)所需滿足的性質(zhì)Φ,是否存在一個控制器使得C（S）|=Φ。CTAV是一個基于時間自動機的實時系統(tǒng)模型檢測工具。CTAV-TGA是在CTAV的基礎上實現(xiàn)的以時間博弈自動機為模型的控制器合成工具。CTAV-TGA實現(xiàn)了以四種基本LTL性質(zhì)<>p,[]p,[]<>p,<>[]p為獲勝目標的控制器合成。但C... 

【文章來源】：蘇州大學江蘇省

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

【學位級別】：碩士

【部分圖文】：

圖１－１?一個簡單的時間博弈自動機??

第二韋祛木概念?找制器合成工具ＣＴＡＶ－ＴＧＡ的功能擴展勹改進??第二章基本概念??開放實時系統(tǒng)的運行狀態(tài)不僅取決于系統(tǒng)自身的行為，而且還受到外界環(huán)境因素??的影響。在模型檢測方法中，通常使用時間自動機對實時系統(tǒng)進行建模，但時間自動??機中所有的動作都是可控的，無法模擬外界環(huán)境因素。因此我們采用時間博弈自動機??作為刻畫開放實時系統(tǒng)的模型，利用時間博弈自動機中的不可控遷移模擬外界環(huán)境因??素。因此在本章中將介紹開放實時系統(tǒng)的概念，時間博弈自動機的相關理論，以及用??于描述性質(zhì)的線性時序邏輯公式。??２．１開放的實時系統(tǒng)??實時系統(tǒng)指的是能夠及時響應外部事件的發(fā)生，并且能在－定時限內(nèi)快速完成對??事件的處理的計算機應用系統(tǒng)。實時系統(tǒng)的行為不僅依賴其計算邏輯的正確性，而且??事件的響應需要滿足一定時間約束。模型檢測所涉及的實時系統(tǒng)一般都是封閉的，在??進行模型檢測時只需遍歷狀態(tài)空間，尋找不滿足指定性質(zhì)的路徑或狀態(tài)。而控制器合??成問題針對的是開放的實時系統(tǒng)，其運行結(jié)果不僅取決于自身的運行狀態(tài)，還受到外??界因素的影響。圖２－１中給出一個開放實時系統(tǒng)的例子。??貯藏室??ｎ??＿升降機??產(chǎn)出帶??Ｉ?Ｉ??機械臂?２?—??１＝＾：．，．?］?生產(chǎn)器??供給帶Ｕ?１??圖２－１?—個簡單的生產(chǎn)單元??以上圖所示的一個用于生產(chǎn)盤子的生產(chǎn)單元［２１］為例，其生產(chǎn)原料通過供給帶源源??８??

控制器合成工具ＣＴＡＶ－ＴＧＡ的功能擴展勹改進?第三章挖制器合成技術坫礎??ｘ＝＝１０??ｘ＝０??ｙ＞＝２〇?一、??，＼?ｘ＝０，ｙ＝０?／?＼?ｘ＝０；ｙ＝０?ｆ’￣＾??Ｓｔａｒｔ?ｊ??＾?Ｌｏｏｐ?：?———Ｂａｄ??ｘ＜＝１０??圖３－１時間自動機??３．２最大值抽象??在３．１節(jié)中定義過一個時間自動機ｄ的符號化語義模型為一個符號化遷移系統(tǒng)??八，Ｇ可能有無窮多個符號化狀態(tài)。可以通過使用某種抽象［１３］方式，將遷移系統(tǒng)轉(zhuǎn)??化為－？個冇窮狀態(tài)遷移系統(tǒng)，從ｉｆｉ丨使得遍歷狀態(tài)空間稱為可能，這是能夠進行模型檢??測以及控制器合成的基矗??如閣３－２中的時間自動機，它只有一個初始狀態(tài)ａ，它的符號化辻移序列為：??Ａ－０?Ａ．ｖ＝０?Ａ．ｙ－ｖ＝〇＞?＾?＜ｃｉ，?１Ｓ６２八〇５．ｖ＾ｌ?八？ｖ－．ｖＭ〉＝＞?＜ａ，２：￡；ｃ５３?／＼０分５１?／＼ｘ－．ｖ＝２＞?＝＞?＜ａ，??３ＳｖＳ４八０￥＾?１八ｊｃ－ｊ＝３＞．．．。雖然榷十時鐘帶的符號化語義使得狀態(tài)空Ｎ變?yōu)榭蓴?shù)的，??但其狀態(tài)空間依然是無窮的。每過去１個時間單元，循環(huán)就會發(fā)生－次，．Ｖ會被重置??為０，同時ｘ在不停的增長，從而導致了一個可數(shù)的，但是卻無限的狀態(tài)空間。??ｙ?■－?〇．?：：：：：??＼?ｒ?：＝?０?－?■＇?■１＇?＂?：?＾??…＜?ｄ＼／／／／／??Ｉ）?１?１?：ｉ?Ｉ?Ｘ??圖３－２簡單的時間自動機和它的狀態(tài)空間??時間Ｇ動機的符號化語義可能引發(fā)一個無窮的遷移系統(tǒng)。設＃足時間自動機的－??個符號化狀態(tài)（／，％中的時鐘帶。為了得到一個乜窮可達圖，我們使用一Ａ抽象ａ：?Ｐ??１７??

【參考文獻】：
期刊論文
[1]基于LTL語義的可達性控制器合成工具[J]. 景麗莎,項周坤.  計算機系統(tǒng)應用. 2016(11)



本文編號：2981363