《電子技術應用》
您所在的位置:首頁 > 嵌入式技術 > 業(yè)界動態(tài) > 基于UML與Petri網(wǎng)的嵌入式系統(tǒng)設計與驗證

基于UML與Petri網(wǎng)的嵌入式系統(tǒng)設計與驗證

2008-05-29
作者:廖曉文,,劉 美

  摘 要: 提出了一種基于UML與Petri網(wǎng)的嵌入式系統(tǒng)" title="嵌入式系統(tǒng)">嵌入式系統(tǒng)設計與驗證的方法,,詳細討論了該方法的主要應用流程,并給出了一個應用實例,。
  關鍵詞: 嵌入式系統(tǒng)設計" title="系統(tǒng)設計">系統(tǒng)設計 UML語言 Petri網(wǎng) 驗證


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


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

?

?

?


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


  本文提出的方法充分發(fā)揮了UML和Petri網(wǎng)的長處,,能夠支持從需求分析到模型實現(xiàn)的全生命周期,。用這種方法為嵌入式系統(tǒng)建模具有以下優(yōu)點:(1)具有模塊化功能和可重用性;(2)實現(xiàn)了對用戶友好的可視化設計;(3)UML模型與計算機程序設計語言聯(lián)系緊密,,易于模型實現(xiàn),。
  由于本文所舉的示例較為簡單,所以可以用手工為其建模,、分析,。對于比較復雜的系統(tǒng)有時需要借助一些計算機輔助工具來建模和分析。目前,,關于Petri 網(wǎng)的計算機輔助工具和基于UML 的可視化建模工具已經(jīng)相當成熟, 但從UML 模型到Petri 網(wǎng)的轉換工具還未出現(xiàn),,作者正在從事這方面的研究工作??梢韵嘈? 隨著這一問題的解決, 集成UML 與Petri網(wǎng)方法在未來嵌入式系統(tǒng)建模領域會發(fā)揮越來越重要的作用,。
參考文獻
1 Douglass B P.RealTime UML:Developing Efficient Objects for Embedded Systems.Unitedstates Addison Wesley,2000
2 Paltor I P,,Lilius J.Digital Sound Recorder:A case study on designing embedded systems using the UML notation.Turku Centre for Computer Science TUCS Technical Report NO 234,,January 1999
3 Rational Software Corporation.Rational Rose Real-time 2002.http://www.rational.com/product/rosert,2002
4 Gomaa H.Designing Concurrent,,Distributed,,and Real-Time Applications with UML.Unit-edstates Addison Wesley,2000

本站內(nèi)容除特別聲明的原創(chuàng)文章之外,,轉載內(nèi)容只為傳遞更多信息,,并不代表本網(wǎng)站贊同其觀點。轉載的所有的文章,、圖片,、音/視頻文件等資料的版權歸版權所有權人所有。本站采用的非本站原創(chuàng)文章及圖片等內(nèi)容無法一一聯(lián)系確認版權者,。如涉及作品內(nèi)容,、版權和其它問題,,請及時通過電子郵件或電話通知我們,,以便迅速采取適當措施,避免給雙方造成不必要的經(jīng)濟損失,。聯(lián)系電話:010-82306118,;郵箱:[email protected]