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

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

?

?

?

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