劉卓媛, 尤 楓, 趙瑞蓮, 尚 穎

(北京化工大學(xué) 信息科學(xué)與技術(shù)學(xué)院, 北京 100029)

1 引言

當(dāng)前, 隨著嵌入式實時軟件在高科技領(lǐng)域(尤其是在航空, 航天和現(xiàn)代武器制造等許多關(guān)鍵領(lǐng)域)的日益增長的應(yīng)用, 人們更加關(guān)注嵌入式實時操作系統(tǒng)的可靠性[1]. 軟件測試是保證軟件質(zhì)量和可靠性的主要手段, 針對實時嵌入式軟件有著不同的測試方法, 其中基于模型的軟件測試技術(shù)由于測試效率高, 并且能夠發(fā)現(xiàn)其他測試技術(shù)難以發(fā)現(xiàn)的故障[2], 常被應(yīng)用于該類軟件的測試.

實時嵌入式軟件不僅具有實時性特征, 而且往往全部或部分表現(xiàn)出基于狀態(tài)的行為[3], 因此針對該類軟件的建模需支持事件驅(qū)動、狀態(tài)轉(zhuǎn)移描述、復(fù)雜動態(tài)交互行為和嚴格的時間限制等領(lǐng)域特征[4]. 近年來, 在實時嵌入式軟件的測試中最常用的模型有FSM、UML、EFSM等. 其中, EFSM模型由于能同時描述被測軟件的控制流和數(shù)據(jù)流信息, 更精確地描述軟件系統(tǒng)的動態(tài)行為[5], 常被用于軟件測試中. 然而, 目前針對該類軟件的基于模型的軟件測試方法仍然存在以下問題:(1)不能完全滿足該類軟件在建模及測試中對實時性的要求； (2)軟件通常非常復(fù)雜, 而目前大多數(shù)研究都是通過分析需求或功能類的文檔去構(gòu)建模型, 通常需要豐富的專業(yè)領(lǐng)域知識, 才能構(gòu)建相對準確和完整的模型, 從而導(dǎo)致建模工作的成本和難度都比較高.

為了解決以上兩大問題, 在基于模型的軟件測試的研究中, 時間自動機[6,7]在FSM模型上為遷移添加了時鐘約束, 為狀態(tài)添加了不變式約束, 以此來描述實時嵌入式軟件的時間特征. 但是, 該模型缺乏對嵌入式軟件行為信息的描述. Yin等人基于EFSM模型提出了RT-EFSM (Real-Time Extended Finite State Machine model)[8,9]模型擴展了EFSM模型中狀態(tài)轉(zhuǎn)換過程中對時間特征的描述, 能夠有效表征嵌入式軟件的實時特性, 但是在建模時需要對功能和需求文檔深入分析,建模成本較高.

而文獻[10]從用戶的角度描述軟件的系統(tǒng)行為,通過記錄用戶使用軟件過程中與軟件交互的場景實例,來描述軟件的主要功能、使用方式以及邊界條件等主要信息[11], 因此基于使用場景構(gòu)建模型既可以相對細致的描述軟件的行為特征, 又不需要考慮軟件內(nèi)部的邏輯結(jié)構(gòu)和特性, 很大程度降低了建模的難度. 在 Wang等人的工作中[12]利用動態(tài)分析獲取用戶與Web應(yīng)用程序之間的交互信息, 將其表征為用戶行為軌跡(trace)并映射到EFSM模型中, 有效實現(xiàn)了面向Web應(yīng)用程序的EFSM模型的構(gòu)建. 因此本文將基于使用場景構(gòu)建實時嵌入式軟件的RT-EFSM模型.

但是, 場景難以覆蓋系統(tǒng)部件實例之間的所有交互[13],特別是需要復(fù)雜的交互才能探究的軟件系統(tǒng)行為. 因此,基于使用場景構(gòu)建的模型大多是不完整的. 為了驗證模型的完整性, 嚴亞偉等人[14]主要針對系統(tǒng)的數(shù)據(jù)完整性進行分析和驗證. 針對數(shù)據(jù)完整性的定量評估問題,提出使用概率計算樹邏輯(PCTL)和馬爾可夫決策過程(MDP)分別對完整性進行形式化的定義和評估, 實現(xiàn)了對完整性的定量驗證, 為系統(tǒng)開發(fā)中的完整性需求提供支持. 文獻[15]提出事件及其執(zhí)行條件可以代表Web應(yīng)用程序的行為, 依據(jù)事件和JS分支覆蓋為Web應(yīng)用程序EFSM模型定義了完整性準則, 對模型的完整性進行評估, 并提出了面向Web應(yīng)用的EFSM模型自動補全方法, 提高了模型的完整性.

綜上, 本文將場景表征為形式化的Scene, 并從中識別出構(gòu)建RT-EFSM模型的狀態(tài)和遷移, 利用狀態(tài)和遷移的等價性有效合并狀態(tài)和遷移并確定遷移中變量條件的上下界, 從而構(gòu)建RT-EFSM模型. 而對于實時嵌入式軟件, 在同一觸發(fā)事件的不同條件下, 會導(dǎo)致系統(tǒng)的狀態(tài)、參數(shù)以及后續(xù)操作發(fā)生不同的變化. 因此該類軟件的動態(tài)行為涉及用戶使用該軟件時觸發(fā)的事件、觸發(fā)事件時的條件、觸發(fā)事件后發(fā)生改變的系統(tǒng)狀態(tài)、參數(shù)及后續(xù)操作. 由于事件和相應(yīng)的執(zhí)行條件共同決定了系統(tǒng)到達的狀態(tài)和后續(xù)操作, 因此它們代表了該類軟件的系統(tǒng)行為, 從而事件及條件的完整性決定了系統(tǒng)行為模型的完整性. 由于RT-EFSM模型中的遷移條件包括時鐘條件和非時鐘條件, 因此, 本文主要根據(jù)時鐘變量條件及非時鐘變量條件來設(shè)計模型完整性準則來驗證模型的完整性, 并利用時鐘變量條件在時間軸[9]上的連續(xù)性以及非時鐘變量條件的對立分支條件生成待補全遷移, 然后在模型上搜索可行的遷移序列以遍歷它們, 通過執(zhí)行生成的遷移序列, 將待補全遷移添加到模型中, 從而提高模型的完整性.

本文的主要貢獻概括如下:

(1)本文基于使用場景Scene自動化構(gòu)建RT-EFSM模型；

(2)本文定義了時鐘變量和非時鐘變量完整性準則來評估嵌入式軟件的RT-EFSM模型的完整性；

(3)針對RT-EFSM模型, 提出了模型的待補全遷移生成策略生成待補全遷移, 并利用模型補全方法將其添加到模型中；

(4)本文以4個實時嵌入式系統(tǒng)為實驗對象進行一系列實驗來驗證所提方法的有效性.

2 基于使用場景的時間擴展EFSM構(gòu)建與完整性驗證方法

2.1 方法整體框架

本文基于實時嵌入式軟件的使用場景對軟件的動態(tài)行為進行建模, 并對模型進行完整性評估及補全, 以保證模型的完整性及后續(xù)測試的有效性. 基于使用場景的時間擴展EFSM構(gòu)建與完整性驗證的方法框架如圖1所示, 主要包括: (1)基于使用場景構(gòu)建RT-EFSM模型； (2)設(shè)計完整性評估準則并對RT-EFSM模型進行完整性驗證； (3)模型補全. 對于不完整的模型, 設(shè)計待補全遷移生成策略生成待補全遷移, 并使用模型補全方法將待補全的遷移添加到模型中, 從而提高模型的完整性.

圖1 基于使用場景的RT-EFSM構(gòu)建與完整性驗證方法框架

2.2 基于使用場景的RT-EFSM模型構(gòu)建

(1)使用場景的規(guī)范化表示

使用場景主要記錄了用戶與系統(tǒng)進行交互時所執(zhí)行的一系列行為活動, 是用例的一個實例, 反映了系統(tǒng)的性能和運行方式[10]. 使用場景一般用自然語言進行描述, 為了自動化地構(gòu)建RT-EFSM模型, 需要對使用場景進行規(guī)范化表示, 本文將其定義為Scene.

定義1. 使用場景(Scene): 一條Scene可以表示為Scene=＜IA0,…,IAj,…,IAn-1＞, 代表用戶與實時嵌入式系統(tǒng)軟件進行的一系列交互.

EScene中的任一交互IAj表示為＜Source,Event,Cond[Vcond,Ccond],Action,Target＞, 其中Source和Target分別表示系統(tǒng)軟件在事件觸發(fā)前后所處的狀態(tài),用一個二元組＜Label,StateName＞表示,Label表示狀態(tài)標(biāo)號,StateName表示狀態(tài)名稱；Event表示用戶執(zhí)行的操作, 即觸發(fā)事件；Cond表示觸發(fā)事件時系統(tǒng)軟件所滿足的條件,Vcond和Ccond分別表示事件發(fā)生時所滿足的變量約束條件和時間約束條件,Action表示系統(tǒng)軟件在事件觸發(fā)后執(zhí)行的響應(yīng)及引起參數(shù)更改的后續(xù)操作.

(2)Scene中的RT-EFSM狀態(tài)與遷移識別

為了構(gòu)建RT-EFSM模型, 需從規(guī)范化的Scene集合中識別模型的狀態(tài)和遷移. 根據(jù)RT-EFSM模型的定義[9], 模型的狀態(tài)集合可表示為S={s0, …,sj, …,sn}, 其中的每一個狀態(tài)sj=＜Label,StateName＞,Label和StateName分別表示狀態(tài)的標(biāo)號和名稱； 遷移集合T={t0,…,tj,…,tn}表示允許模型從一個狀態(tài)遷移到另一個狀態(tài)的交互信息集合, 集合中的任一遷移表示為tj=＜Head(tj),Event(tj),Cond(tj),Action(tj),Tail(tj)＞. 因此,Scene中的任一交互IAj可視為模型中的遷移tj,IAj中的Source與Target可分別對應(yīng)tj的Head(tj)與Tail(tj), ＜Event,Cond[Vcond,Ccond],Action＞對應(yīng)于tj中的＜Event(tj),Cond(tj),Action(tj)＞. 從而當(dāng)遍歷完Scene集合中的每一條Scene時, 可獲得RT-EFSM模型的狀態(tài)列表S和遷移列表T.

(3)基于使用場景的RT-EFSM模型構(gòu)建

根據(jù)上節(jié)分析, 根據(jù)Scene集合可獲取RT-EFSM模型的狀態(tài)列表S和遷移列表T. 但是由于用戶與系統(tǒng)可能存在多次重復(fù)的交互, 所以收集的Scene集合中的Scene之間可能存在相同的交互信息, 從而導(dǎo)致獲取的狀態(tài)列表和遷移列表中可能會包含相同的狀態(tài)或遷移.因此, 合并狀態(tài)和遷移是構(gòu)建RT-EFSM模型的關(guān)鍵.

根據(jù)對Scene集合的進一步分析, 由于嵌入式軟件的實時性, 用戶的某些操作必須在特定的時間內(nèi)完成, 但是每一條Scene記錄的只是在某一時間點用戶與系統(tǒng)軟件的交互信息. 因此, 在一定的時間范圍內(nèi),用戶觸發(fā)相同的事件后系統(tǒng)軟件的狀態(tài)變化和相應(yīng)的響應(yīng)是相同的； 而超過了某一時間點時, 即使觸發(fā)相同的事件, 卻會導(dǎo)致系統(tǒng)軟件的狀態(tài)和響應(yīng)不同. 而這種實時性表征為遷移tj中的時鐘變量等式的不同取值.因此遷移的合并過程中需要根據(jù)時鐘變量的值集確定時間約束, 即遷移的合并可能涉及時鐘約束的派生.

同樣, 對于系統(tǒng)軟件有次數(shù)限制的操作, 用戶與系統(tǒng)軟件進行交互的次數(shù)最終表征為模型遷移tj中計數(shù)器變量[16]等式的不同取值, 因此遷移的合并過程中需要根據(jù)計數(shù)器變量的值集確定計數(shù)器變量約束, 即遷移的合并可能涉及非時鐘變量約束的派生.

為了有效合并遷移列表T并確定遷移的時鐘約束和非時鐘約束, 本文提出了等價遷移和弱等價遷移概念, 其定義如下:

定義2. 等價遷移: 給定遷移t1=＜Head(t1),lbl(t1),Tail(t1)＞和t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中標(biāo)簽lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 當(dāng)且僅當(dāng)Head(t1)=Head(t2),lb(t1)=lb(t2), 且Tail(t1)=Tail(t2)時,t1與t2等價.

定義3. 弱等價遷移: 給定遷移t1=＜Head(t1),lbl(t1),Tail(t1)＞和t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中標(biāo)簽lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC],當(dāng)且僅當(dāng)Head(t1)=Head(t2),lbl(t1)～lbl(t2),且Tail(t1)=Tail(t2)時,t1與t2弱等價. 其中l(wèi)bl(t1)～lbl(t2)表示標(biāo)簽信息中除Cond(t1)中的時鐘變量和計數(shù)器變量與Cond(t2)中對應(yīng)的同一變量的取值不同外, 其余各個組成部分均相等.

根據(jù)等價遷移和弱等價遷移的定義, 遍歷遷移列表T, 識別出其中的等價遷移及弱等價遷移, 并對這兩種遷移進行合并. 在弱等價遷移的合并過程中, 能夠派生出遷移的時間約束及計數(shù)器變量約束. 其派生過程如下: 遍歷由多個互為弱等價遷移組成的弱等價遷移列表, 抽取其中的時鐘變量和計數(shù)器變量及其取值, 獲得＜var,valueSet＞對, 其中var代表某一變量,valueSet代表該變量的值集. 對于變量var確定其值集valueSet的最小邊界值MIN和最大邊界值MAX, 從而派生出變量var滿足的約束為: MIN≤var≤MAX. 當(dāng)確定時間約束及計數(shù)器變量約束后, 將弱等價遷移列表中的每一條遷移tj上的時鐘變量及計數(shù)器變量等式修改為派生的時間約束和計數(shù)器變量約束, 從而將弱等價遷移列表變?yōu)榈葍r遷移列表, 實現(xiàn)了弱等價遷移的合并.

為了實現(xiàn)基于使用場景構(gòu)建RT-EFSM模型, 設(shè)計了算法1, 從使用場景中識別模型的狀態(tài)和遷移, 并合并等價狀態(tài)和遷移, 最終得到RT-EFSM模型.

算法1. RT-EFSM模型構(gòu)建算法1) 將使用場景表示為規(guī)范化的Scene, 獲得場景的Scene集合；2) 識別Scene集合中RT-EFSM的狀態(tài)及遷移, 獲得其狀態(tài)列表S及遷移列表T；3) 采用距離公式(本文采用編輯距離)對狀態(tài)列表S中的任意兩個狀態(tài)的狀態(tài)名稱進行字符串比較, 判斷兩個狀態(tài)節(jié)點是否為同一狀態(tài). 若相同, 則刪除狀態(tài)標(biāo)號較大的狀態(tài), 獲得無相同狀態(tài)的狀態(tài)集合S′, 并修訂遷移列表中的相應(yīng)狀態(tài), 獲得新的遷移列表T′；

4) 遍歷遷移列表T′中的遷移, 將遷移列表T′中當(dāng)前遷移t與列表中后面的遷移的各個組成部分一一比較, 如果存在互為弱等價或互為等價的遷移, 則將它們加入到遷移列表T1′中, 如果不存在, 則將添加到T′′中；5) 合并遷移列表T1′中的遷移將其變?yōu)榈葍r遷移列表T1′′, 保留T1′′中的其中一條遷移添加到遷移T′′, 實現(xiàn)等價遷移的合并, 返回第4)步.6) 最終獲得狀態(tài)集合S′以及遷移集合T′′, 即RT-EFSM模型.

2.3 基于使用場景構(gòu)建的RT-EFSM模型完整性驗證

(1)模型完整性準則

由于使用場景Scene難以涵蓋應(yīng)用系統(tǒng)的所有行為, 因此很難保證基于Scene構(gòu)建的RT-EFSM的模型的完整性. 由于事件及其執(zhí)行條件的完整性決定了系統(tǒng)行為模型的完整性, 因此,本文基于RT-EFSM模型遷移t上的條件Cond(t)中的時間約束以及變量約束條件考慮模型的完整性, 提出了模型完整性評估準則.

定義4. 時間約束對立遷移: 給定遷移t1=＜Head(t1),lbl(t1),Tail(t1)＞,t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中標(biāo)簽lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 如果Head(t1)=Head(t2),Tail(t1)!=Tail(t2),lb1(t)中的觸發(fā)事件Event(t)相同, 且Cond(t1)與Cond(t2)中的同一時鐘變量c的時間約束不同, 那么稱t1和t2為時鐘變量c的時間約束對立遷移.

根據(jù)如上定義, 互為時間約束對立遷移的多個遷移組成時鐘變量c的時間約束對立遷移集TRc.

定義5. 時區(qū)[9]: 設(shè)RT-EFSM模型中實時嵌入式軟件中狀態(tài)轉(zhuǎn)換時鐘集合為L, 則L的取值范圍為[0,+∞). 分布在L時間軸上的時間點L1,L2,…,Lk(L1＜L2＜…＜Lk)將時鐘集合L劃分為k+1個子區(qū)域, 其中每一個子區(qū)域稱為一個時區(qū).

根據(jù)如上定義以及圖2的時區(qū)劃分可知, 對于時間約束L1＜ω1＜L2和L2≤ω2＜L3, 分布在時鐘集合L時間軸上的時區(qū)是連續(xù)的.

圖2 時區(qū)劃分

定義6. 變量約束對立遷移: 給定遷移t1=＜Head(t1),lbl(t1),Tail(t1)＞,t2=＜Head(t2),lbl(t2),Tail(t2)＞, 其中標(biāo)簽lbl(t)=＜Event(t),Cond(t),Action(t)＞,Cond(t)=[VC,TC], 如果Head(t1)=Head(t2),Tail(t1)!=Tail(t2),lb1(t)中的觸發(fā)事件Event(t)相同, 且Cond(t1)與Cond(t2)中的同一非時鐘變量v的約束相反, 那么稱t1和t2為變量v的變量約束對立遷移.

根據(jù)上述定義, 本文提出的時間約束完整性準則以及變量約束完整性準則定義如下:

定義7. 時間約束完整性準則: 假設(shè)RT-EFSM模型上的遷移集合為T={t1,t2,…,tj,…,tn}(n＞0), 對于任意一條遷移tj, 如果tj上的任意時鐘變量c存在時間約束對立遷移集TRc, 并且TRc中c的所有時間約束分布在時鐘集合L時間軸上的時區(qū)是連續(xù)的, 則稱該模型滿足時間約束完整性準則.

定義8. 變量約束完整性準則: 假設(shè)RT-EFSM模型上的遷移集合為T={t1,t2,…,tj,…,tn}(n＞0), 對于任意一條遷移tj, 如果tj上的任意非時鐘變量v存在變量約束對立遷移, 則稱該模型滿足變量約束完整性準則.

根據(jù)以上兩種準則, 通過對已構(gòu)建的RT-EFSM模型的遷移進行靜態(tài)分析并進行完整性驗證. 通過靜態(tài)分析獲得造成模型不完整的時間約束或變量約束及其所在的遷移, 根據(jù)這些信息對模型進行補全.

(2)待補全遷移生成

對于不完整的模型, 其時間約束的時區(qū)分布不連續(xù)或者變量約束的對立約束不存在, 即模型沒有表征在不連續(xù)的時區(qū)范圍內(nèi)或變量約束的對立約束下軟件的動態(tài)行為. 因此, 本文提出了最近鄰時間約束遷移生成策略以及對立變量約束遷移生成策略, 生成待補全遷移并將其補充到RT-EFSM模型中.

① 最近鄰時間約束遷移生成策略

假設(shè)造成RT-EFSM模型不完整的時間約束為p0≤c≤p1, 其所在的遷移為t, 則可以根據(jù)時鐘變量c的時間約束對立遷移集TR獲得該變量的時間約束在時鐘集合L時間軸上的時區(qū)分布, 從而得到與遷移t的時間約束分布最近鄰的時區(qū)及其所在遷移[p2,p3](t1),[p4,p5](t2)(其中p3＜p0,p1＜p4), 由于模型缺少對處于不連續(xù)時區(qū)(p3,p0)∪(p1,p4)中的時間點的軟件行為進行表征. 因此待補全遷移表征在當(dāng)前時區(qū)的最近鄰時區(qū)表示的時間約束下, 觸發(fā)相同的事件并滿足相同的變量約束條件時, 系統(tǒng)可能的動態(tài)行為. 因此設(shè)待補全遷移的時間約束為p3＜c＜p0,p1＜c＜p4,構(gòu)造的待補全遷移如式(1)所示:

② 對立變量約束遷移生成策略

假設(shè)造成RT-EFSM模型不完整的非時鐘變量v的約束為VC, 其所在的遷移為t, 構(gòu)造的待補全遷移表征為當(dāng)該遷移的變量約束與遷移t的變量約束VC相反時, 在相同的源狀態(tài)下, 觸發(fā)相同的事件并滿足相同的時鐘約束條件, 系統(tǒng)可能的動態(tài)行為. 因此構(gòu)造的待補全的遷移如式(2)所示:

根據(jù)這兩個遷移補全策略, 生成了待補全的遷移列表Tf. 為了提高模型的完整性, 需要將其添加到RTEFSM模型中.

(3) RT-EFSM模型補全

為了將生成的待補全遷移列表Tf中的遷移添加到模型中, 需要識別其后續(xù)狀態(tài)和操作[15], 并通過動態(tài)執(zhí)行可行遷移序列來遍歷待補全遷移. 即模型補全方法如下: 對于Tf= {t0,…,tj,…,tn} (n＞0)中的每一條遷移tj,找到該遷移的源節(jié)點在原模型中的位置, 以該遷移作為初始遷移, 通過前向搜索生成可行遷移序列[16], 并利用GA算法找到觸發(fā)該序列的輸入數(shù)據(jù)[17], 使遷移序列與遷移數(shù)據(jù)共同構(gòu)成可執(zhí)行路徑. 并將可執(zhí)行路徑作為具體的測試實例, 對其進行動態(tài)執(zhí)行, 從執(zhí)行結(jié)果中識別待補全遷移觸發(fā)的狀態(tài)和后續(xù)操作.

如果觸發(fā)狀態(tài)與所建立的RT-EFSM模型中某一狀態(tài)相同, 即它們的狀態(tài)名稱相同, 則將該狀態(tài)作為補全遷移的目標(biāo)狀態(tài). 否則, 觸發(fā)狀態(tài)為新狀態(tài), 則將此狀態(tài)添加到RT-EFSM模型的狀態(tài)集合S中, 并將補全遷移的目標(biāo)狀態(tài)設(shè)置為新狀態(tài).

綜上, 模型完整性驗證與補全算法如算法2所示.

算法2. RT-EFSM模型完整性驗證與補全算法1) 遍歷模型的遷移及遷移上的時鐘約束和變量約束, 獲取模型遷移上的時鐘約束對立遷移TR； 獲取模型遷移上未找到變量約束對立遷移的遷移集CR.

2) 根據(jù)TR與CR以及待補全遷移生成策略生成待補全遷移集Tf.3) 對于Tf中的每一條遷移tj, 判斷是否能夠在RT-EFSM模型中找到一條可執(zhí)行遷移路徑來觸發(fā)tj, 如果能找到, 則將該遷移補全到模型中, 否則將該待補全遷移tj放置在Tf 的最后, 考慮另一個待補全遷移.4) 如果Tf中所有待補全遷移擁有其相應(yīng)的可執(zhí)行遷移序列, 或者達到了時間預(yù)算, 那么模型補全就終止了.

3 實驗分析

3.1 實驗設(shè)計

(1)研究問題

為了驗證本文所提方法的有效性, 實驗部分主要解決以下兩個主要問題:

研究問題1: 基于使用場景構(gòu)建RT-EFSM模型的方法是否有效? 該方法的時間效率如何?

研究問題2: 本文提出的待補全遷移生成策略是否有效?

(2)實驗對象

本文將4個實時嵌入式系統(tǒng)作為實驗對象, 包括ATM 機、三層樓的綜合電梯系統(tǒng)、簡易飛行安全系統(tǒng)及飛機發(fā)動機控制軟件. 表1為4個嵌入式系統(tǒng)的使用場景的詳細信息, 包括實時系統(tǒng)名稱、使用場景總數(shù)、Scene列表中包含的交互總數(shù)、狀態(tài)總數(shù)、事件總數(shù).

表1 嵌入式系統(tǒng)的使用場景信息

(3)評估指標(biāo)

① 由于用戶與實時嵌入式系統(tǒng)的交互是通過事件實現(xiàn)的, 事件及其執(zhí)行條件導(dǎo)致系統(tǒng)的不同響應(yīng). 而使用場景記錄了用戶與系統(tǒng)進行交互時所執(zhí)行的一系列行為活動, 是用例的一個實例. 可以看出, 軟件的系統(tǒng)行為與事件及使用場景密切相關(guān). 因此, 為了驗證建模方法的有效性, 即生成的模型是否將使用場景Scene集合中包含的信息完整表征出來, 該信息不僅包括每一次用戶與系統(tǒng)軟件進行交互的信息, 還包括使用場景所表示的可行執(zhí)行序列. 因此, 本文提出了事件覆蓋率(Event Coverage,EC)和場景覆蓋率(Scene Coverage,SC)兩個度量指標(biāo)來衡量本文提出的模型構(gòu)建方法的有效性.

事件覆蓋率(Event Coverage,EC),EC衡量RT-EFSM模型中出現(xiàn)的事件占Scene集合中的所有事件的比例:

其中, |RT.Event|表示生成的RT-EFSM模型中包含的事件數(shù), |S.scene|表示在Scene集合中的總事件數(shù).

場景覆蓋率(Scene Coverage,SC),SC表示Scene集合中能夠被基于RT-EFSM模型生成的可執(zhí)行測試路徑覆蓋的Scene條數(shù)占總Scene條數(shù)的比例:

其中, |RT.scene|表示被基于RT-EFSM模型生成的測試路徑覆蓋的Scene條數(shù), |S.scene|表示在Scene集合中的總Scene條數(shù).

② 本文的模型補全方法認為, 待補全遷移成功添加到模型中的標(biāo)準是通過對模型的動態(tài)執(zhí)行生成可行遷移序列來遍歷待補全遷移. 即在模型中能夠找到一條從初始節(jié)點開始到待補全遷移的可執(zhí)行序列并生成可執(zhí)行測試路徑. 因此, 為了評估待補全遷移生成策略的有效性, 即根據(jù)該策略生成的待補全遷移能夠成功添加到模型中, 本文提出了待補全遷移可行率(for Complete Transition Feasibility,fCTF)的評估指標(biāo).

待補全遷移可行率(for Complete Transition Feasibility,fCTF)表示待補全遷移列表中能夠被在原RTEFSM模型中動態(tài)模擬執(zhí)行生成的可執(zhí)行測試路徑觸發(fā)的待補全遷移條數(shù)占待補全遷移總數(shù)的比例:

其中, |Executable Paths Number|表示能夠被基于RTEFSM模型生成的可執(zhí)行測試路徑觸發(fā)的待補全遷移條數(shù), |forComplete Transition Number|表示待補全遷移列表中的待補全遷移總數(shù).

3.2 實驗結(jié)果與分析

對研究問題1, 根據(jù)4個實時嵌入式系統(tǒng)的Scene集合構(gòu)建其RT-EFSM模型. 如圖3所示是根據(jù)ATM系統(tǒng)的使用場景Scene集合構(gòu)建的RT-EFSM模型. 該模型中的節(jié)點代表模型的狀態(tài), 其中同心圓節(jié)點代表模型的初始節(jié)點, 邊代表模型的遷移, 由模型的一個狀態(tài)節(jié)點指向另一個節(jié)點. 例如圖中的S0代表模型的初始節(jié)點, T1表示模型的一個遷移.

圖3 ATM系統(tǒng)的RT-EFSM模型

表2顯示了ATM系統(tǒng)的RT-EFSM模型的遷移信息, 包括遷移的源節(jié)點Head(t), 目標(biāo)節(jié)點Tail(t),觸發(fā)事件Event(t), 遷移轉(zhuǎn)換條件Cond(t), 以及系統(tǒng)響應(yīng)及操作Action(t). 通過本文的模型構(gòu)建方法, 可以將從初始Scene集合中包含了198個狀態(tài)和157個遷移,在合并相同的狀態(tài)和遷移之后, 狀態(tài)和遷移分別減少為5和19, 其中的一個狀態(tài)表示ATM系統(tǒng)的一個功能頁面, 例如S0表示“輸入密碼頁面”, 實現(xiàn)了狀態(tài)、遷移的有效合并.

表2 ATM系統(tǒng)RT-EFSM模型遷移信息

如表3所示統(tǒng)計了使用本文提出的建模方法構(gòu)建的4個系統(tǒng)的RT-EFSM模型的相關(guān)信息及時間效率,包括系統(tǒng)名稱、模型的狀態(tài)數(shù)量、遷移數(shù)量、事件覆蓋率(EC)、場景覆蓋率(SC)以及建模的時間開銷.

表3 模型構(gòu)建的結(jié)果及時間效率分析

結(jié)合表1和表3可以看出, 本文的建模方法可以有效縮減模型的狀態(tài)和遷移數(shù), 例如三層樓的綜合電梯系統(tǒng)的Scene集合中包含的狀態(tài)數(shù)和遷移數(shù)分別為118和100, 而所建的RT-EFSM模型中狀態(tài)和遷移數(shù)減少到5和25； 簡易飛行安全系統(tǒng)的Scene集合中包含的狀態(tài)數(shù)和遷移數(shù)分別為297和261, 所建模型中的狀態(tài)和遷移分別減少到5和34. 除了狀態(tài)及遷移的數(shù)量外, 我們利用兩個衡量指標(biāo), 即事件覆蓋率(EC)和場景覆蓋率(SC)來度量各模型的覆蓋情況, 以驗證模型構(gòu)建方法的有效性. 如表3的實驗結(jié)果所示, 利用Scene構(gòu)建的模型的EC和SC均為100%. 即本文提出的建模方法可以保留Scene集合中的所有事件和場景表示的執(zhí)行序列信息. 此外, 針對4個實時嵌入式系統(tǒng),模型構(gòu)建的最大時間開銷是0.5070 s, 時間成本是可以接受的.

綜上, 本文提出的模型構(gòu)建方法可以有效合并Scene集合中的相同狀態(tài)和遷移, 同時保證了RT-EFSM模型對實時嵌入式軟件動態(tài)行為的覆蓋且時間開銷較小.因此, 基于使用場景構(gòu)建RT-EFSM的方法可以有效建立實時嵌入式軟件的行為模型.

對于研究問題2, 為了評價本文提出的待補全生成策略的有效性, 本文統(tǒng)計了根據(jù)待補全遷移生成策略生成的待補全遷移數(shù)量、能夠被基于RT-EFSM模型生成的可執(zhí)行測試路徑觸發(fā)的待補全遷移條數(shù)(EPN),以及待補全遷移可行率 (fCTF)和不可行率(nfCTF), 其中不可行率nfCTF=1-fCTF.

由表4所示可以看出, 根據(jù)本文提出的待補全遷移生成策略可以生成待補全遷移, 例如該策略為ATM系統(tǒng)生成的待補全遷移數(shù)為16, 能夠被基于模型生成的可執(zhí)行測試路徑觸發(fā)的待補全遷移條數(shù)為15. 為三層樓的綜合電梯系統(tǒng)生成了10個待補全遷移, 其中有7條待補全遷移能夠被基于模型生成的可執(zhí)行測試路徑觸發(fā). 另一方面, 通過fCTF和nfCTF兩個指標(biāo)評估待補全遷移生成策略的有效性. 例如, 簡易飛行安全系統(tǒng)的待補全遷移可行率為86.67%, 不可行遷移可行率為13.33%. 飛機發(fā)動機控制軟件的待補全遷移可行率為78.57%, 不可行遷移可行率為21.43%. 其中fCTF最低為70.00%,nfCTF最高為30.00%, 并且各個實時系統(tǒng)的待補全遷移可行率都遠遠高于其不可行率, 從而說明本文提出的待補全遷移策略能夠生成待補全的遷移, 并且生成的待補全遷移的可行率較高, 即待補全遷移能夠有效補全到模型中.

表4 待補全遷移策略的有效性分析

4 結(jié)論與展望

本文提出了一種基于使用場景自動構(gòu)建RT-EFSM模型的方法, 設(shè)計了模型完整性驗證的準則, 并通過該準則驗證模型的完整性. 針對不完整的模型, 利用待補全遷移生成策略生成待補全的遷移, 并利用模型補全算法將其填補到模型中. 本文完成了4個實時系統(tǒng)模型的構(gòu)建與完整性驗證, 實驗表明本文提出的自動建模方法可以將用戶使用場景集中的冗余狀態(tài)和遷移進行有效的合并, 花費的時間開銷較小. 并且根據(jù)待補全遷移策略生成的待補全遷移能夠有效補全到模型中,從而提高了模型的完整性. 在后續(xù)工作中, 將擴大實驗規(guī)模, 并進一步優(yōu)化補全模型的方法和策略, 從而提高本文方法的有效性.