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

【文章來(lái)源】：蘇州大學(xué)江蘇省

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

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

【部分圖文】：

圖１－１?一個(gè)簡(jiǎn)單的時(shí)間博弈自動(dòng)機(jī)??

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

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

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



本文編號(hào)：2981363