在嵌入式系統設計中采用模型的方法，有利于保證系統的正確性，縮短開發周期，降低開發費用。作為面向對象的建模技術，統一建模語言UML可以將復雜的系統設計簡單化，并能從需求分析、設計到實現等各階段為嵌入式系統開發人員提供有力支持。但UML缺乏精確的語義描述，因此無法對用UML建立的嵌入式" title="的嵌入式">的嵌入式系統模型進行形式化的分析和驗證。Petri網建模方法基于嚴格的數學理論，使用形式化規范對系統建模，并且可以通過眾多的工具完成驗證。但Petri網建模方法不直觀,在需求獲取、交流等方面存在無法克服的弱點。
　　UML與Petri網相結合的建模方法能實現二者互補，既能有效獲取需求、分析設計，又能進行嚴格建模、形式化驗證。UML與Petri網結合建模的主要研究和應用都集中于工作流的建模。本文在上述背景下研究了基于UML和Petri網的嵌入式系統設計與驗證的方法。
1 相關研究
　　目前，已經有幾種影響比較大的、基于UML的、用于嵌入式系統設計的語言和建模方法，如RTUML、COMET、ROPES。
　　在嵌入式系統的UML模型檢驗方面，也出現了一些利用UML的狀態圖" title="狀態圖">狀態圖對模型進行檢驗的方法。這些方法都是把UML的狀態圖翻譯為現有模型檢驗工具的輸入語言(如SPIN、SMV)后加以驗證，但對模型而言，它們不是最自然、最有效的方法。首先它忽視了系統的靜態結構特征；其次，翻譯后會引入較多的冗余，而且由于意義不同需要額外處理。并且這種只能檢驗部分性質的方法涉及到許多形式化內容，一般軟件開發人員難以掌握。因此，這種方法的使用范圍相當有限。
　　隨著嵌入式系統的廣泛應用，產生了多種擴充的Petri網模型。其中，最典型的有OPNets(Object Oriented High-Level Petri Nets)、ETPN(Extended Time Petri Nets)和PRES(Petri net based Representation for Embedded Systems)。
　　由于自身的原因，Petri網在捕獲用戶的需求、實現細節與需求分開、交流等方面有難以克服的弱點。同時，Petri網只是一種用來描述和分析系統模型的工具,不是計算機的實現工具,必須采用一定的方法通過軟件才能實現。
2 方法架構
　　本文針對嵌入式系統實時、并發、事件驅動等特性，借鑒COMET、ROPES、OPNets、ETPN和PRES等影響比較大的、基于UML或者Petri網的嵌入式系統設計建模方法，提出UML與Petri網的嵌入式系統設計與驗證方案。其方法構架如圖1所示。

　　具體說明如下：
　　(1)創建系統協作圖(環境圖，Context Diagram)以說明對象/數據的輸入輸出。創建需求可追蹤性表，列出需求名、需求號、引用、用例、UML元素、測試實例、描述、職責等。給出評審管理計劃、時間表、風險、命名/編碼標準、方法設計(過程/構造型/特征/約束)。這部分是可選的，也可以通過相關的替代方式來描述。
　　(2)充分利用用例描述系統需求。嵌入式系統需要與外部環境交互。重要的外部對象及其對系統的交互構成系統需求分析的基礎。在需求描述階段不考慮設計因素，只定義系統各方面的行為。這個階段相當于一般的嵌入式系統設計中的產品定義階段。
　　(3)分析需求，確定硬件和軟件之間的分界(即軟硬件劃分)，創建一個高級的系統體系結構，將復雜控制算法精化和特征化。劃分完后進入硬件設計階段，可按上所述設計過程開發硬件。相對簡單的系統可以跳過這一步驟。
　　(4)利用UML的靜態圖描述系統的靜態模型。定義系統中對象的類、類的屬性、類之間的關系及每個類的操作。
　　(5)對象分析，確定參與每一個用例的對象及相互間關系。對象可以是實體對象、接口對象(設備接口、用戶接口、系統接口)、控制對象和應用邏輯對象。
　　(6)利用UML的動態圖描述系統的動態模型。開發對象的交互圖，顯示參與用例的對象之間交互的次序，分析對象間交互的次序及傳送的信息。同時，為每個狀態依賴協作圖中的對象開發一個狀態圖，識別這些關鍵抽象如何響應外部和內部激勵，以及它們如何動態協作以獲得系統級的功能。
　　(7)進入設計建模階段，綜合分析模型，采用迭代的方式得到整個軟件的體系結構。
　　(8)將類圖和狀態圖轉換為相應Petri網模型并分析驗證。如模型不正確，則需重新審視其設計。如果正確，則進行構件映射，以節約此后相關開發的時間。對于構件，應按照可重用的要求進行設計、實現、打包和編寫文檔。
　　由于嵌入式系統通常為實時系統，而且許多嵌入式系統特別強調程序的實時特性，因此，設計一個嵌入式系統時需要考慮此系統是否有時間的限制。這些時間限制可能是局部的或者是全局的，區別在于這個時間限制相對于整個系統的位置。在編寫程序時，必須滿足這些限制，避免實際執行時超出時間限制所造成的影響。在這方面，可以將序列圖轉換為時間Petri網來進行程序排程驗證。此外，對于內部交互比較復雜的子系統，為達到良好的建模效果，可直接運用OPNets進行設計，使子系統開發實現形式化與可視化，同時使建模、模擬與運行一體化。
3 應用實例
　　本文所舉應用示例為：商家擁有三臺客戶稅控機" title="稅控機">稅控機，一臺服務器稅控機，服務器稅控機直接控制兩臺發票打印機，為有需要的顧客打印發票。即顧客向客戶機操作員提出申請，操作員向服務器稅控機申請執行相關操作，服務器稅控機將要打印的發票信息輸送到兩臺打印機中的一臺，顧客到發票打印機處取發票。為節約成本，客戶端采用8位單片機，服務器采用32位單片機。
　　按照前面所述方法，建立了系統相關的類圖和狀態圖，如圖2、圖3、圖4、圖5所示。

?

?

?

　　在描述狀態圖和類圖方面，本文遵循的原則為：事件(events)和動作(actions)必須表示為有效的方法(methods)。一個狀態圖中的類能夠監聽請求其方法(request(＜method＞) )的事件，也能夠發出所請求的方法已完成(commit(＜method＞))的信號。對于狀態圖中的動作，既可以是請求一個外部服務(request(＜method＞))，也可以是執行一個方法(ser(＜method＞))。
　　通過將UML圖映射到Petri網，便可以對UML定義采取嚴格正式的分析了。Petri網支持多種不同開銷和精度的分析方法，如模擬、可達樹、關聯矩陣、狀態方程。這里主要討論動態方面的主要技術:模擬、可達樹。
　　模擬包括建立一個使燃順序并將其表示為UML狀態。模擬要耗費相當的計算資源并且是自動化的。它能夠揭示缺陷，并為最終用戶提供重要的信息反饋，因此它支持對定義的驗證。例如，通過圖6所示的Petri網進行模擬可以使用戶理解系統的最終行為，因此能夠在早期驗證定義發現可能存在的問題。通過分析圖6的模擬執行序列，可以發現這個模型明顯不正確，因為它可以允許顧客打印與他們所購買商品不同的發票清單。在本例中，問題可以追溯到設計時的錯誤:軟件工程師沒有指定顧客應該到哪一個打印機取發票，因此Customer1可以到Printer2打印發票，而實際上Printer2是為Customer2開的。通過模擬可以發現問題，但不能保證不會出現與預期不相符的行為。
　　可達樹用以描述Petri網的可達(標識)集，它既與Petri網的結構有關，也與Petri網的初始標識有關。通過分析Petri網的可達樹，可了解Petri網的許多重要性質，如有界性、安全性、守恒性、可達性、覆蓋性甚至死鎖和活性等。對從UML模型轉換過來的Petri網模型，可達樹法還可以保證類定義性，被證明是一種有效的分析方法。但它窮舉所有有限的可能狀態進行計算，因此只適合驗證比較小的Petri網系統。對于一般的嵌入式系統而言，利用模擬分析的方法已足夠。
　　同時，對于內部交互比較復雜的子系統，可以直接運用OPNets進行設計和驗證。