嵌入式系統(tǒng)構(gòu)件pdf-初探一種構(gòu)件化嵌入式軟件設(shè)計(jì)模型驗(yàn)證工具

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

本文基于接口自動(dòng)機(jī)模型對(duì)構(gòu)件化嵌入式軟件設(shè)計(jì)（CBESD:Component-BasedEmbeddedSoftwareDesigns）的分析與驗(yàn)證方法展開進(jìn)一步研究，在Eclipse開放平臺(tái)上實(shí)現(xiàn)了一個(gè)CBESD的模型分析與驗(yàn)證原型工具T-CBESD（aToolforComponent-basedEmbeddedSoftwareDesigns）。該工具的目的是應(yīng)用于構(gòu)件化嵌入式軟件開發(fā)的設(shè)計(jì)建模階段，對(duì)設(shè)計(jì)者所關(guān)心的系統(tǒng)重要功能性質(zhì)以及與時(shí)間相關(guān)的實(shí)時(shí)行為性質(zhì)進(jìn)行嚴(yán)格形式化分析和驗(yàn)證，提高系統(tǒng)可靠性的可信度。

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

2.工具的理論基礎(chǔ)軟件工程中的構(gòu)件化設(shè)計(jì)方法學(xué)通過(guò)復(fù)用和組合軟件模塊來(lái)構(gòu)造系統(tǒng)，從而提高系統(tǒng)開發(fā)效率和可靠性。通常，一個(gè)復(fù)雜的嵌入式系統(tǒng)由多個(gè)計(jì)算子系統(tǒng)構(gòu)成，其軟件系統(tǒng)也具有較高的構(gòu)件化特征，因此，構(gòu)件化的設(shè)計(jì)已成為解決嵌入式軟件設(shè)計(jì)復(fù)雜性問(wèn)題的一種手段。與此同時(shí)，構(gòu)件接口之間的交互場(chǎng)景也成為體現(xiàn)系統(tǒng)行為復(fù)雜性的一個(gè)重要方面。

本文中所討論的原型工具就是使用形式化的接口自動(dòng)機(jī)模型來(lái)對(duì)系統(tǒng)構(gòu)件接口動(dòng)態(tài)行為進(jìn)行設(shè)計(jì)建模，并使用UML交互概觀圖模型來(lái)描述多種基于場(chǎng)景的構(gòu)件交互行為規(guī)約，然后應(yīng)用形式化分析算法對(duì)設(shè)計(jì)模型是否滿足系統(tǒng)規(guī)約進(jìn)行分析和驗(yàn)證。2.1建模系統(tǒng)構(gòu)件以及組合行為

接口自動(dòng)機(jī)（interfaceautomata，簡(jiǎn)稱IA）是用來(lái)刻畫軟件構(gòu)件接口交互行為時(shí)序特征的一種形式化語(yǔ)言。它描述了一個(gè)構(gòu)件被使用的時(shí)候其對(duì)外界環(huán)境的輸入假設(shè)和輸出保證，即構(gòu)件內(nèi)方法被調(diào)用的先后次序以及構(gòu)件對(duì)外環(huán)境輸出調(diào)用信息或結(jié)果的次序。

輸入動(dòng)作可以用來(lái)建模：1）構(gòu)件內(nèi)可以被調(diào)用的方法或過(guò)程；2）通信信道的接收端；3）調(diào)用外部過(guò)程的返回等。輸出動(dòng)作可以用來(lái)建模：1）對(duì)其他構(gòu)件中的方法或過(guò)程的調(diào)用；2）通信信道的發(fā)送消息端；3）構(gòu)件中方法或過(guò)程的調(diào)用結(jié)束時(shí)的返回；4）構(gòu)件中方法或過(guò)程執(zhí)行中出現(xiàn)的異常返回，等。內(nèi)部動(dòng)作則表達(dá)了兩個(gè)構(gòu)件在組合過(guò)程中的同步交互行為。

考慮到嵌入式軟件的實(shí)時(shí)性建模需求，需要對(duì)IA進(jìn)行實(shí)時(shí)語(yǔ)義的擴(kuò)展，以增強(qiáng)接口自動(dòng)機(jī)對(duì)實(shí)時(shí)系統(tǒng)的描述能力。直觀上，對(duì)接口自動(dòng)機(jī)每一個(gè)轉(zhuǎn)換添加時(shí)間區(qū)間約束，以表示此轉(zhuǎn)換發(fā)生的最小、最大時(shí)限；擴(kuò)展后的模型稱為實(shí)時(shí)接口自動(dòng)機(jī)。

我們使用接口自動(dòng)機(jī)的組合狀態(tài)空間來(lái)表達(dá)多構(gòu)件系統(tǒng)的組合行為；自動(dòng)機(jī)組合狀態(tài)空間中每一條可能的狀態(tài)轉(zhuǎn)換序列用來(lái)表達(dá)多構(gòu)件系統(tǒng)的一個(gè)組合行為軌跡。基本IA和擴(kuò)展的RTIA組合狀態(tài)空間的定義略有不同，以下只給出了RTIA組合空間（實(shí)時(shí)接口自動(dòng)機(jī)網(wǎng)絡(luò)）的定義；不帶時(shí)間語(yǔ)義的基本接口自動(dòng)機(jī)的組合定義參見文獻(xiàn)。2.2基于場(chǎng)景的交互行為規(guī)約

在基于場(chǎng)景的系統(tǒng)規(guī)約中，通常將一個(gè)系統(tǒng)相對(duì)獨(dú)立的功能模塊建模為一個(gè)場(chǎng)景描述。這個(gè)場(chǎng)景表達(dá)了參與其中的各構(gòu)件之間如何進(jìn)行交互。進(jìn)一步的，在系統(tǒng)設(shè)計(jì)階段，還會(huì)關(guān)心有多個(gè)簡(jiǎn)單場(chǎng)景組合起來(lái)的復(fù)雜場(chǎng)景需求，即需要考慮多個(gè)簡(jiǎn)單場(chǎng)景之間的邏輯關(guān)系。

交互概觀圖（InteractionOverviewDiagrams）是在UML2規(guī)范中引入的一種用以描述系統(tǒng)中復(fù)雜交互場(chǎng)景的動(dòng)態(tài)行為模型。交互概觀圖本質(zhì)上是將活動(dòng)圖模型與順序圖模型結(jié)合在一起，圖中的每一個(gè)節(jié)點(diǎn)都可以視為一個(gè)用順序圖表達(dá)的簡(jiǎn)單交互場(chǎng)景，然后利用活動(dòng)圖所提供的順序、迭代、并發(fā)、選擇等操作將多個(gè)不同的順序圖場(chǎng)景聯(lián)系在一起；這樣就可以用來(lái)表達(dá)語(yǔ)義更為豐富的系統(tǒng)交互行為。在本文中所關(guān)心的以下幾種場(chǎng)景組合一致性問(wèn)題都可以用交互概觀圖來(lái)有效的描述：

1.存在一致性：某個(gè)特定的場(chǎng)景D是否在系統(tǒng)所有行為中至少出現(xiàn)一次，或者某個(gè)指定的場(chǎng)景D是否在系統(tǒng)的所有行為中一定不會(huì)出現(xiàn)。

2.前向強(qiáng)制一致性：當(dāng)某個(gè)條件場(chǎng)景D1出現(xiàn)時(shí)，則場(chǎng)景D2一定會(huì)隨之在系統(tǒng)后續(xù)行為中發(fā)生。

3.逆向強(qiáng)制一致性：當(dāng)某個(gè)條件場(chǎng)景D1出現(xiàn)時(shí)，則場(chǎng)景D2一定在D1之前就在系統(tǒng)的行為中發(fā)生。

4.雙向強(qiáng)制一致性：當(dāng)兩個(gè)條件場(chǎng)景D1、D2在系統(tǒng)一個(gè)行為中先后出現(xiàn)時(shí)，則在這兩個(gè)場(chǎng)景之間一定有D3發(fā)生。2.3模型分析與驗(yàn)證算法

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

3.T-CBESD的設(shè)計(jì)與實(shí)現(xiàn)基于以上的理論分析與驗(yàn)證框架，本文設(shè)計(jì)了一個(gè)原型工具T-CBESD（aToolforComponent-BasedEmbeddedSoftwareDesigns）。T-CBESD的目的是應(yīng)用于構(gòu)件化嵌入式軟件開發(fā)的設(shè)計(jì)建模階段，對(duì)設(shè)計(jì)者所關(guān)心的一些系統(tǒng)重要功能性質(zhì)以及與時(shí)間相關(guān)的實(shí)時(shí)行為性質(zhì)進(jìn)行嚴(yán)格形式化分析和驗(yàn)證，以提高系統(tǒng)可靠性的可信度。工具的基本設(shè)計(jì)原則主要包括以下兩個(gè)方面：

T-CBESD應(yīng)當(dāng)具備跨平臺(tái)運(yùn)行、易擴(kuò)展特征：即工具應(yīng)該可以盡可能在多種不同運(yùn)行平臺(tái)上運(yùn)行，并且考慮到在未來(lái)工作中，我們將在目前的工作基礎(chǔ)上對(duì)接口自動(dòng)機(jī)模型進(jìn)行資源以及能耗等語(yǔ)義描述方面的進(jìn)一步擴(kuò)展；因此，選擇了面向?qū)ο蟪绦蛟O(shè)計(jì)語(yǔ)言Java作為工具的實(shí)現(xiàn)語(yǔ)言。Java具有良好的跨平臺(tái)運(yùn)行特征以及豐富的類庫(kù)資源，并可以使用面向?qū)ο蟪绦蛟O(shè)計(jì)思想中的類繼承等方法對(duì)工具進(jìn)行方便可靠的擴(kuò)展。

T-CBESD應(yīng)當(dāng)具備易使用、易維護(hù)特征：用戶可以比較方便的使用工具，或進(jìn)行調(diào)整；因此，選擇了工業(yè)界廣泛使用的開放集成開發(fā)環(huán)境Eclipse作為工具的運(yùn)行平臺(tái)，即使用Eclipse的插件（plug-in）技術(shù)來(lái)設(shè)計(jì)和開發(fā)T-CBESD。用戶可以很容易在Eclipse環(huán)境中通過(guò)插件技術(shù)來(lái)安裝、配置和使用工具；同時(shí)，在T-CBESD的輸入輸出接口中所使用的XML語(yǔ)言在Java和Eclipse環(huán)境中也是得到完全的支持。

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

輸入輸出接口；UML順序圖模型的預(yù)處理；自動(dòng)機(jī)組合模型的建立；非實(shí)時(shí)功能驗(yàn)證算法的實(shí)現(xiàn)；實(shí)時(shí)功能驗(yàn)證算法的實(shí)現(xiàn)等。以下分別給出詳細(xì)說(shuō)明。3.1輸入輸出接口設(shè)計(jì)

T-CBESD的輸入輸出均是以XML文件形式來(lái)描述的系統(tǒng)設(shè)計(jì)模型、系統(tǒng)需求規(guī)約以及驗(yàn)證結(jié)果信息等。其中，工具的輸入包括：描述系統(tǒng)設(shè)計(jì)的接口自動(dòng)機(jī)模型的XML文件和描述系統(tǒng)規(guī)約的消息交互序列的XML文件；輸出則包括：描述系統(tǒng)組合行為的接口自動(dòng)機(jī)組合模型的XML文件和包含驗(yàn)證結(jié)果信息的XML文件。這里，最核心部分是接口自動(dòng)機(jī)模型的XML文件格式的設(shè)計(jì)。在圖3中給出了一個(gè)非實(shí)時(shí)構(gòu)件基本接口自動(dòng)機(jī)模型的XML文件示例說(shuō)明；通過(guò)XML的樹形標(biāo)簽格式，分別定義了自動(dòng)機(jī)名、自動(dòng)機(jī)個(gè)數(shù)（如果這是一個(gè)組合自動(dòng)機(jī)）、狀態(tài)個(gè)數(shù)、狀態(tài)名、后繼狀態(tài)名、轉(zhuǎn)換個(gè)數(shù)、轉(zhuǎn)換名、轉(zhuǎn)換的出發(fā)和到達(dá)狀態(tài)名、動(dòng)作個(gè)數(shù)、動(dòng)作名、動(dòng)作類型等數(shù)據(jù)信息，用來(lái)完整準(zhǔn)確的保存接口自動(dòng)機(jī)模型的語(yǔ)義信息。此外，對(duì)于擴(kuò)展的實(shí)時(shí)接口自動(dòng)機(jī)模型，其相應(yīng)的XML文件格式定義中還包含與動(dòng)作相關(guān)聯(lián)的時(shí)間區(qū)間約束標(biāo)記。

在上述定義的XML文件基礎(chǔ)上，就可以使用Java類庫(kù)中的DOM（文檔對(duì)象模型）方法很方便的對(duì)自動(dòng)機(jī)模型進(jìn)行解析及生成。例如：在T-CBESD中設(shè)計(jì)了parseXmlDocument（）和parseRtXmlDocument（）兩