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

【文章來源】：西華大學四川省

【文章頁數】：70 頁

【學位級別】：碩士

【部分圖文】：

面向對象模型

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

解電梯的運行情況以后，根據電梯的運行策略，建立電梯的模型。在 OOT，包含若干個對象類，一個對象類就是一個 Petri 網的子系統，而對象類的顏色集和托肯集綜合表示；操作可以用變遷來表示。為了以后電梯控制系統方便，在這里首先按照面向對象的技術對系統進行分類。電梯控制系統按照為三大類，類及類之間關系的結構圖如圖 5.2 所示。


本文編號：2906442