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

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

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

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

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

【部分圖文】：

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

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

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


本文編號：2906442