嵌入式系統構件pdf-初探一種構件化嵌入式軟件設計模型驗證工具

1.引言嵌入式計算系統已經廣泛的應用于生活中的各個領域，如：交通、能源、醫療、控制、通信、軍事等。近年來隨著計算機硬件性能的不斷提高，嵌入式系統中軟件的規模和復雜性不斷增加，使軟件對整個系統的影響逐漸占據了統治地位。關鍵系統中的嵌入式軟件失效將會導致生命與財產的重大損失。因此，嵌入式軟件通常具有極高的功能可靠性、嚴格的實時性等要求，如何保證系統同時滿足給定的功能和非功能需求已成為當前高可信嵌入式計算領域中的研究熱點。目前，工業界已有一些比較有效的嵌入式軟件測試和調試方法（如：在處理器中嵌入ICE功能，調試代理軟件，JTAG模擬等）。但從軟件工程的角度來看，這些方法都是在系統的開發中后期階段所使用，而在嵌入式軟件設計與分析的前期階段還缺乏有效的方法和工具對系統設計進行分析與驗證。

本文基于接口自動機模型對構件化嵌入式軟件設計（CBESD:Component-BasedEmbeddedSoftwareDesigns）的分析與驗證方法展開進一步研究，在Eclipse開放平臺上實現了一個CBESD的模型分析與驗證原型工具T-CBESD（aToolforComponent-basedEmbeddedSoftwareDesigns）。該工具的目的是應用于構件化嵌入式軟件開發的設計建模階段，對設計者所關心的系統重要功能性質以及與時間相關的實時行為性質進行嚴格形式化分析和驗證，提高系統可靠性的可信度。

本文內容安排如下：第2節中給出了非實時功能行為驗證以及實時功能行為驗證的理論基礎，包括：描述系統動態行為的多種接口自動機模型，基于場景的系統規約描述模型，以及形式化分析與驗證的抽象算法等。在第3節中給出了原型工具T-CBESD的基本設計思想，非實時功能行為驗證模塊以及實時功能行為驗證模塊的設計與實現，包括：工具輸入輸出接口設計、狀態空間數據結構設計、基于場景的系統規約模型的輸入預處理、具體驗證算法的設計與實現等。第4節中給出了應用實例研究；最后是相關工作比較和結束語，對本文中原型工具的特點、意義以及進一步的工作進行簡要討論。

2.工具的理論基礎軟件工程中的構件化設計方法學通過復用和組合軟件模塊來構造系統，從而提高系統開發效率和可靠性。通常，一個復雜的嵌入式系統由多個計算子系統構成，其軟件系統也具有較高的構件化特征，因此，構件化的設計已成為解決嵌入式軟件設計復雜性問題的一種手段。與此同時，構件接口之間的交互場景也成為體現系統行為復雜性的一個重要方面。

本文中所討論的原型工具就是使用形式化的接口自動機模型來對系統構件接口動態行為進行設計建模，并使用UML交互概觀圖模型來描述多種基于場景的構件交互行為規約，然后應用形式化分析算法對設計模型是否滿足系統規約進行分析和驗證。2.1建模系統構件以及組合行為

接口自動機（interfaceautomata，簡稱IA）是用來刻畫軟件構件接口交互行為時序特征的一種形式化語言。它描述了一個構件被使用的時候其對外界環境的輸入假設和輸出保證，即構件內方法被調用的先后次序以及構件對外環境輸出調用信息或結果的次序。

輸入動作可以用來建模：1）構件內可以被調用的方法或過程；2）通信信道的接收端；3）調用外部過程的返回等。輸出動作可以用來建模：1）對其他構件中的方法或過程的調用；2）通信信道的發送消息端；3）構件中方法或過程的調用結束時的返回；4）構件中方法或過程執行中出現的異常返回，等。內部動作則表達了兩個構件在組合過程中的同步交互行為。

考慮到嵌入式軟件的實時性建模需求，需要對IA進行實時語義的擴展，以增強接口自動機對實時系統的描述能力。直觀上，對接口自動機每一個轉換添加時間區間約束，以表示此轉換發生的最小、最大時限；擴展后的模型稱為實時接口自動機。

我們使用接口自動機的組合狀態空間來表達多構件系統的組合行為；自動機組合狀態空間中每一條可能的狀態轉換序列用來表達多構件系統的一個組合行為軌跡。基本IA和擴展的RTIA組合狀態空間的定義略有不同，以下只給出了RTIA組合空間（實時接口自動機網絡）的定義；不帶時間語義的基本接口自動機的組合定義參見文獻。2.2基于場景的交互行為規約

在基于場景的系統規約中，通常將一個系統相對獨立的功能模塊建模為一個場景描述。這個場景表達了參與其中的各構件之間如何進行交互。進一步的，在系統設計階段，還會關心有多個簡單場景組合起來的復雜場景需求，即需要考慮多個簡單場景之間的邏輯關系。

交互概觀圖（InteractionOverviewDiagrams）是在UML2規范中引入的一種用以描述系統中復雜交互場景的動態行為模型。交互概觀圖本質上是將活動圖模型與順序圖模型結合在一起，圖中的每一個節點都可以視為一個用順序圖表達的簡單交互場景，然后利用活動圖所提供的順序、迭代、并發、選擇等操作將多個不同的順序圖場景聯系在一起；這樣就可以用來表達語義更為豐富的系統交互行為。在本文中所關心的以下幾種場景組合一致性問題都可以用交互概觀圖來有效的描述：

1.存在一致性：某個特定的場景D是否在系統所有行為中至少出現一次，或者某個指定的場景D是否在系統的所有行為中一定不會出現。

2.前向強制一致性：當某個條件場景D1出現時，則場景D2一定會隨之在系統后續行為中發生。

3.逆向強制一致性：當某個條件場景D1出現時，則場景D2一定在D1之前就在系統的行為中發生。

4.雙向強制一致性：當兩個條件場景D1、D2在系統一個行為中先后出現時，則在這兩個場景之間一定有D3發生。2.3模型分析與驗證算法

基于以上給出的接口自動機系統組合行為模型以及交互場景系統規約模型，可以對2.2節中提出的多個基于功能的一致性驗證問題進行分析與驗證；同時，考慮嵌入式軟件設計中的實時需求，以上每個基于功能的一致性驗證問題都存在一個相應的帶時間約束的版本；即在完成功能性驗證的同時，也必須同時滿足交互場景中給定的時間約束。在相關研究工作中，對上述幾類模型驗證問題進行了形式化定義和分析，并分別設計了相應的驗證算法。算法的基本思想是對帶有不同語義信息的系統組合行為的狀態空間進行搜索，將每一個可能的系統行為與基于場景的交互規約進行比較，來判斷設計模型是否滿足各種系統規約。例如：對于存在一致性驗證問題，如果在組合狀態空間中順序圖D所描述場景中的消息事件序列至少出現一次，則判定系統行為滿足D，其相應的抽象算法框架參見文獻中的算法；其中所提到的投影路徑是為了處理狀態空間中環路的出現導致所檢驗的系統行為路徑可能是無窮長度的問題。對于系統實時行為的驗證算法，則需要進一步考慮由于時間的引入所帶來的如何將連續時間進行整型化處理，以及帶時間約束的投影路徑的建立；RTIA-Network的一致性驗證抽象算法框架參見文獻。中國代寫論文網與您分享論文范文

3.T-CBESD的設計與實現基于以上的理論分析與驗證框架，本文設計了一個原型工具T-CBESD（aToolforComponent-BasedEmbeddedSoftwareDesigns）。T-CBESD的目的是應用于構件化嵌入式軟件開發的設計建模階段，對設計者所關心的一些系統重要功能性質以及與時間相關的實時行為性質進行嚴格形式化分析和驗證，以提高系統可靠性的可信度。工具的基本設計原則主要包括以下兩個方面：

T-CBESD應當具備跨平臺運行、易擴展特征：即工具應該可以盡可能在多種不同運行平臺上運行，并且考慮到在未來工作中，我們將在目前的工作基礎上對接口自動機模型進行資源以及能耗等語義描述方面的進一步擴展；因此，選擇了面向對象程序設計語言Java作為工具的實現語言。Java具有良好的跨平臺運行特征以及豐富的類庫資源，并可以使用面向對象程序設計思想中的類繼承等方法對工具進行方便可靠的擴展。

T-CBESD應當具備易使用、易維護特征：用戶可以比較方便的使用工具，或進行調整；因此，選擇了工業界廣泛使用的開放集成開發環境Eclipse作為工具的運行平臺，即使用Eclipse的插件（plug-in）技術來設計和開發T-CBESD。用戶可以很容易在Eclipse環境中通過插件技術來安裝、配置和使用工具；同時，在T-CBESD的輸入輸出接口中所使用的XML語言在Java和Eclipse環境中也是得到完全的支持。

主要的邏輯處理框架包括：

輸入輸出接口；UML順序圖模型的預處理；自動機組合模型的建立；非實時功能驗證算法的實現；實時功能驗證算法的實現等。以下分別給出詳細說明。3.1輸入輸出接口設計

T-CBESD的輸入輸出均是以XML文件形式來描述的系統設計模型、系統需求規約以及驗證結果信息等。其中，工具的輸入包括：描述系統設計的接口自動機模型的XML文件和描述系統規約的消息交互序列的XML文件；輸出則包括：描述系統組合行為的接口自動機組合模型的XML文件和包含驗證結果信息的XML文件。這里，最核心部分是接口自動機模型的XML文件格式的設計。在圖3中給出了一個非實時構件基本接口自動機模型的XML文件示例說明；通過XML的樹形標簽格式，分別定義了自動機名、自動機個數（如果這是一個組合自動機）、狀態個數、狀態名、后繼狀態名、轉換個數、轉換名、轉換的出發和到達狀態名、動作個數、動作名、動作類型等數據信息，用來完整準確的保存接口自動機模型的語義信息。此外，對于擴展的實時接口自動機模型，其相應的XML文件格式定義中還包含與動作相關聯的時間區間約束標記。

在上述定義的XML文件基礎上，就可以使用Java類庫中的DOM（文檔對象模型）方法很方便的對自動機模型進行解析及生成。例如：在T-CBESD中設計了parseXmlDocument（）和parseRtXmlDocument（）兩