發(fā)布時(shí)間：2020-12-09 06:27

　　嵌入式系統(tǒng),作為計(jì)算機(jī)技術(shù)中的一項(xiàng)重要研究方向,已經(jīng)被廣泛地應(yīng)用到各個(gè)領(lǐng)域。隨著嵌入式產(chǎn)品在不同領(lǐng)域的應(yīng)用,用戶需求的不斷增加,嵌入式系統(tǒng)功能越來越強(qiáng)大,設(shè)計(jì)難度也越來越大,導(dǎo)致傳統(tǒng)的設(shè)計(jì)方法難以滿足復(fù)雜嵌入式系統(tǒng)的設(shè)計(jì)需求,因此研究系統(tǒng)級(jí)的設(shè)計(jì)方法已成為嵌入式系統(tǒng)設(shè)計(jì)的主要研究方向。本文通過對(duì)現(xiàn)有嵌入式系統(tǒng)建模方法的研究,分析其特點(diǎn)和不足,引出形式化建模是嵌入式系統(tǒng)建模研究的主要方向。針對(duì)基本Petri網(wǎng)在嵌入式系統(tǒng)建模中處理數(shù)據(jù)能力弱、沒有考慮時(shí)間因素和沒有層次結(jié)構(gòu)的問題,通過引入面向?qū)ο蠹夹g(shù)、時(shí)延網(wǎng)和有色網(wǎng),擴(kuò)展了基本Petri網(wǎng),給出了面向?qū)ο蟮臅r(shí)延有色Petri網(wǎng)(OOTCPN)模型的形式化定義。與其他模型相比,本文模型在數(shù)據(jù)描述能力、實(shí)時(shí)性、層次性等方面有了較大的提高,適合復(fù)雜的嵌入式系統(tǒng)建模。在模型驗(yàn)證方面,通過對(duì)基本Petri網(wǎng)模型的驗(yàn)證技術(shù)研究,分別闡述了仿真分析和模型檢驗(yàn)方法的原理和特點(diǎn),探討了Petri網(wǎng)模型的電路仿真分析方法,給出了利用硬件描述語言描述OOTCPN模型的方法,并通過實(shí)例說明。與傳統(tǒng)的Petri網(wǎng)仿真分析軟件相比,此方法適用范圍更廣,可移植性強(qiáng),使... 

【文章來源】：西華大學(xué)四川省

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

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

【部分圖文】：

面向?qū)ο竽Ｐ?br>

圖 4.8 仿真圖Fig. 4.8 Simulation diagram4.3 模型檢驗(yàn)技術(shù)模型檢驗(yàn)是關(guān)于系統(tǒng)性質(zhì)驗(yàn)證的算法和方法[43]。在完整的系統(tǒng)屬性的驗(yàn)證框架下，通常采用狀態(tài)空間搜索的方法來檢測(cè)模型是否滿足用時(shí)序邏輯公式表示的特定性質(zhì)。由于模型檢驗(yàn)的方法在許多方面如電信系統(tǒng)和硬件系統(tǒng)的驗(yàn)證等取得了成功，得到了越來越多的人關(guān)注；并且，隨著計(jì)算機(jī)不斷的發(fā)展和軟件算法的不斷優(yōu)化，該方法展示出廣泛的應(yīng)用前景。與模型檢驗(yàn)相關(guān)的是時(shí)態(tài)邏輯，時(shí)態(tài)邏輯是模型檢驗(yàn)的基礎(chǔ)，是對(duì)系統(tǒng)屬性的形式化表示。在時(shí)態(tài)邏輯中，時(shí)間特性并沒有顯示的表現(xiàn)出來，相反，在公式中可能會(huì)描述某一個(gè)特定狀態(tài)最終會(huì)到達(dá)，或者描述某一個(gè)錯(cuò)誤狀態(tài)從不會(huì)到達(dá)。通過分支時(shí)間的觀點(diǎn)和線性時(shí)間方法可以把時(shí)態(tài)邏輯分為兩個(gè)主要部分：CTL(計(jì)算樹邏輯)和 LTL(線性時(shí)態(tài)邏輯)。4.3.1 計(jì)算樹邏輯

解電梯的運(yùn)行情況以后，根據(jù)電梯的運(yùn)行策略，建立電梯的模型。在 OOT，包含若干個(gè)對(duì)象類，一個(gè)對(duì)象類就是一個(gè) Petri 網(wǎng)的子系統(tǒng)，而對(duì)象類的顏色集和托肯集綜合表示；操作可以用變遷來表示。為了以后電梯控制系統(tǒng)方便，在這里首先按照面向?qū)ο蟮募夹g(shù)對(duì)系統(tǒng)進(jìn)行分類。電梯控制系統(tǒng)按照為三大類，類及類之間關(guān)系的結(jié)構(gòu)圖如圖 5.2 所示。


本文編號(hào)：2906442