可信軟件實時性測試用例集生成方法研究

摘 要：基于RAISE規范語言（RSL）的一個變體——時間化RAISE規范語言（TRSL），提出一種可信軟件實時性測試用例集生成方法。該方法首先去除基于TRSL軟件規約中的抽象時間因素；然后使用劃分分析的方法構造測試單元；再利用動態約束求解方法動態構造具有時間約束的構造項和觀測項，并在此基礎上構建完整的基于TRSL規約的實時性測試用例集。

關鍵詞：時間化RAISE規范語言； 實時性； 可信軟件； 測試用例

中圖分類號：TP311文獻標志碼：A

文章編號：1001-3695(2009)06-2344-03

doi:10.3969/j.issn.1001-3695.2009.06.103

Research of real-time test case generation method of trusted software

CAI Qiong， LI Xing-guo， DING Shuai

(School of Management， Hefei University of Technology， Hefei 230009， China)

Abstract:

This paper provided an approach to derive RTTC from TRSL specification， which was a variant of RSL (RAISE specification language). Firstly， removed abstract time factors from software specification， which was depicted by TRSL. Se-condly， applied partition analysis to generate test data. Then used improvement of OGT algorithm to generate constructive term (CT) and observable term (OT)， which had time constraint. Finally， constructed complete real-time test case based on TRSL specification.

Key words：TRSL; real-time; trusted software; test case

可信軟件是指軟件系統的運行行為及其結果總是符合人們的預期，在受到干擾時仍能提供連續服務的軟件^[1]。軟件的諸多可信性質（如可靠性、防危性、實時性等^[1]）和可信軟件自身具有的復雜性、開放性、階段性、演化性決定了可信軟件測試的復雜性。實時性測試是可信軟件測試過程中最重要的一部分，而測試用例集的生成又是測試過程中代價最大、難度最高的一個研究課題，所以怎樣構造有效的實時性測試用例集是可信軟件測試過程中首要解決的問題。由于可信軟件的概念才剛剛提出，可信軟件實時性測試領域可供借鑒的研究成果不多，但傳統實時系統測試用例集的生成技術已經趨于成熟，其中一些針對時間因素的處理方法值得借鑒。

軟件的時間約束增加了分析軟件可能行為的難度，造成針對可信軟件的實時性測試具有極大的困難。隨著時序邏輯(temporal logic)、時間自動機(timed automata)、時間標號遷移系統(timed labeled transition system，TLTS)等時間相關模型理論的成熟，人們開始研究如何利用時間相關模型對實時系統進行測試和驗證。文獻[2]提出一種增加時間度量的時序邏輯，并基于這一邏輯給出測試用例生成方法。該方法首先對時間進行離散化處理，并根據系統歷史信息生成測試用例。文獻[3]提出一種基于TLTS的測試用例生成方法，首先將TLTS模型轉換為一個標號遷移系統，然后使用W-方法來生成測試用例。文獻[4]采用TA的一種變種——時間安全輸入/輸出自動機(timed safety input/output automata，TSIOA)作為系統的形式模型，并基于此模型構造和執行測試用例。

以上這些都是解決軟件實時性測試問題的有效方法，但其中所選用的形式化語言或模型存在兩方面的不足：a)與時間相關的軟件功能事務描述不明確;b)規約語言難以被賦予語義。這些就會導致軟件的規約描述不準確、測試用例集難以被使用等問題。

運用實時系統測試方法中的時間因素處理理念，選用更為成熟的形式化語言是本文研究可信軟件實時性測試用例生成方法的基礎。RSL是一種廣譜的語言，它既可以用于書寫非常抽象的、初級的規約，也可以用于書寫易于轉換到程序語言的抽象級別較低的規約^[5]。使用RSL最顯著的優點是：從系統描述到設計的大部分軟件過程都能用同一種形式化方法，這既保證了軟件規約形式化描述的正確性，也保證了基于RSL的測試方法可以輕松被執行。TRSL是RSL的擴展版，將時序邏輯與RSL進行融合，在RSL的基礎上添加了許多用于處理時間因素的語言描述和處理邏輯，可以用來精確描述具有時間特性的軟件系統。本文將介紹一種基于TRSL的可信軟件實時性測試用例(real-time test case，RTTC)的生成方法。

1 基本概念^[5]及一個簡單的例子

定義1 Major type（主類型）。假定T={T1，…，Tn}是模塊S中所有類型的集合。如果在Tk的類型表述中存在Ts （1≤k， s≤n），則稱Tk依附于Ts；如果存在Ti（1≤i≤n），且沒有T是依附于Ti，則稱Ti是主類型。

定義2 Function（函數）。可以被定義為四元組：V =〈I， O ，P ， R〉。其中：I代表輸入參數集合；O代表輸出參數集合；P代表函數運行前置條件的值表述；R是函數體或者是函數運行的后置條件。

定義3 Axiom（公理）。可以被定義為四元組：A =〈Ul， Op ，Ur， Pre〉。其中：Ul和Ur分別代表公理左邊和右邊的值表述；Pre代表前置條件；Op代表運算符號。通常情況下，Op是等價符號（≡）或蘊涵符號（）。在RSL或TRSL規約中，公理主要是定義軟件執行動作的形式化描述，是測試的對象。

定義4 Creator（構造器）、observer（解析器）、modifier（重構器）。假定Tm是主類型，若函數V的輸出參數中包含Tm，而輸入參數中不包含，則稱V為構造器；若函數V的輸出參數不包含Tm，而輸入參數中包含，則稱V為解析器；若函數V的輸出參數和輸入參數都包含Tm，則稱V為重構器。

定義5 Wait r表示將其串行后續公理的執行開始時間延遲r個單位時間。

下面通過一個經典的例子來展現基于TRSL的形式化描述方法，這個例子由Chris George^[6]首先提出。

一個簡單的警報系統，它可以被開啟（enable）或關閉（disable）。當系統開啟時，如果有侵擾（disturb），就會響起警報（alarm）;當系統關閉時，就會忽略侵擾。其中時間要求是：在系統開啟后必須經過T1時間，侵擾才能引起警報，并且警報必須在侵擾發生T2時間后才能響起；如果系統被關閉，就不會響起警報。這種時間要求可能被用于建筑或汽車的防盜系統中。T1運行，開啟系統并離開，并不至于引起警報；T2運行，進入建筑（汽車）并在警報響起之前關閉系統。篇幅有限，這里只給出報警系統形式化規約的片斷，如下：

scheme A_ALARM=

 class

type

Alarm，Alarm_state==disabled|enabled|alam…

value

:Time#8226;＞0.0

T1:Time#8226;T1＞，

T2:Time#8226;T2＞，

reset:Real#8226;reset＜0.0…

Axiom

init:Unit→in any write any Unit

init()≡ldisable();main()，

main:Unit→in any write any Unit

main ()≡

while true do

let(x，t)=enable?in

st:=enable; since_disturb:=reset;

since_enable:=0.0;wait();since_enable:=

end

let(x，t)=disable?in

st:=disabled;since_disturb:=reset;

since_enable:=reset;wait()

end

let(x，t)=disturb?in

timing(t);

if st=enabled∧since_enable≥T1∧since_disturb＜0.0

then since_disturb:=0.0

end;

wait();timing()

end

wait timing()

end

timing:Time→write any Unit

timing(t)≡

……

2 基于timed RSL的實時性測試用例生成方法

實時性是指軟件在指定時間內完成反應或提交輸出的能力^[2]，是可信軟件特別是實時安全關鍵軟件需要重點考察的可信性質。

為了有針對性地解決從基于TRSL的規約中生成RTTC的問題，本文假定：a)用于測試的規約具有很好的TRSL描述格式；b)規約中只存在一個屬于抽象數據類型的主類型，而且至少存在一個構造器、解析器和重構器；c)基于TRSL的形式化規約具有時間一致性，且不存在嵌套的情況，如果規約的時間特性存在沖突，則說明規約描述有錯誤；d)本文提到的表達式是公理中可以執行的，且具有函數調用形式的語句，表達式的時間延遲量近似于函數本身的時間約束量；e)Time{|r:real#8226;r≥0.0|}是TRSL中表示時間的系統類型，其最大類型是real，為了計算和表達方便，假定文中提及的時間量屬于Real類型。

2.1 方法概述

基于TRSL的實時性測試用例生成方法的步驟如下：

a）分析基于TRSL的形式化規約，去除抽象時間因素，并構造將相關時間變量與原表達式結合生成具有時間約束的新表達式。

b）采用FMT算法找出規約中的主類型，同時確定規約中的creator、observer、modifier。

c）運用劃分分析的方法將測試輸入域劃分子域，并對子域約束中除主類型之外的所有輸入變量進行實例化。

d）給定常量k，采用線性約束求解的方法動態構建具有時間約束且長度不超過k的CT和OT。

e）構造具有時間約束的RTTC。

本方法可以以增量的方法進行，最終生成的RTTC的具體程度與相應TRSL規約的描述精化程度相關。

2.2 去除抽象時間因素

TRSL規約中采用wait表達式來描述軟件中執行序列之間的抽象時間因素，這些因素多表示后續表達式的執行需要經過一個時間延遲，并不能確定具體的時間量。實際上，從測試實時性的角度來說，TRSL規約中每一個表達式都應該存在相應的時間約束，包括規約中可見的wait表達式以及隱藏的時間量（如函數執行時間量）。

為了簡化規約和有針對性地測試軟件的實時性，可以先將TRSL規約中的抽象時間因素去除，之后計算表達式時間約束變量，并將它與原表達式合并生成新的表達式。本文定義的用于去除抽象時間因素的WTI算法如下：

(1) WipeTimeIng

(2) begin

(3) w = {W1， W2，…， Wn}

(4) for i = 1 to n

(5)if Wi = wait then

(6)let wait (i) = Unit in t end

(7)ti := ti-1 + t +∫;q := q+1;Wi := Wi+1

(8)else ti := ti-1 +∫

(9)end

(10)end for

(11)for j := 1 to n-q

(12)Wj := Wj ∧ tj

(13)end For

(14) end

算法中：W = {W1， W2，…， Wn}代表規約中表達式的集合；∫代表一個給定的隱藏時間量（可以通過計算事先給定，或直接規定一時間常量）。（4）～（10）步用于將抽象時間因素從規約中去除；（11）～（13）將計算獲得的相應時間約束量（或延遲量）與原表達式合并。使用WTI算法，最終獲得一組包含時間變量的新表達式Wt ＝{Wt1 ，Wt2， …，Wtn}。

2.3 劃分子域并實例化子域約束

通過定義4可以直接在形式化規約中指定構造器Vm、解析器Vo、重構器Vc。運用文獻7中給出的GMT算法可以很輕松地從規約中找出模塊的主類型Tm。

也可運用文獻[7]中提出的劃分分析方法將輸入域進行劃分，針對每一個子域給出一個約束CDi =p1∧p2∧…∧pm。其中：pi是一個由變量組成的謂詞。實例化子域約束中的參數，生成待測TRSL規約的測試單元集TCag（x）。

2.1節提出的方案中b） c)都可以運用已有的方法進行解決。這些不是本文的研究重點，不再贅述。

2.4 構造具有時間約束的OT和CT

定義6 Constructive term(構造項，CT)、observable term(觀測項，OT)。Tm(主類型)的構造項是指替代作為輸入變量的Tm 的一個函數調用序列，它是以構造器開始，之后迭代調用重構器（其中，構造器和重構器都是規約中的函數）。Tm（主類型）的觀測項也是一個函數調用序列，它使用構造項對輸入變量Tm進行實例化，之后調用解析器進行封裝。

CT=π(Vm1(…，π(Vm2(…，π(Vmn(…，π(Vcj)))))))

OT=π(Vok(…，π(Vm1(…，π(Vm2(…，π(Vmn(…，π(Vcj)))))))))

構造項和觀測項反映了軟件的一個可能的動作序列，同時也是構造測試用例的基礎，所以計算OT和CT的時間約束是構建RTTC的關鍵。

為了執行測試，需要確定表達式中輸入變量時間約束的具體值；為了提供判斷軟件運行時的時間約束是否滿足系統的要求，需要給出輸出變量時間約束的具體值。而TRSL規約中所有相關的時間約束都是線性的，所以本文采用線性約束求解方法來對OT和CT時間變量的取值進行求解。

本文給出了一個改進的OGT算法（基于RSL的OT生成算法^[7]），在構造OT的同時，計算OT運行所需的時間約束量T∫，并將兩者表達式形式合并。

OTGetTime

begin

 Give positive integer k

 Select fm(Vci)∈{fm(Vc)}

 CT :=fm(Vci)

 T∫ := calculate Time(Vci) +Exp( T∫ )

 x:= 1

 repeat Select fo(Vol)∈{fo(Vo)}

Replace all input variables of Tm in fo(Vol)with CT

while true do T∫ := calculate Time(Vol) + T∫

OT :=fo(Vol)∧Exp(T∫ ) Return OT

Select fm(Vmj)∈{fm(Vm)}

Replace all input variables of Tm in fm(Vmj)with CT

while true do T∫ := calculate Time(Vol) + T∫

CT := fm(Vmj)∧Exp(T∫ )

x:=x+1

 until x>k-1

 end

具有時間約束的CT的構造算法與OTGT算法類似，這里不再單獨介紹。

2.5 構建RTTC

定義7 根據TRSL自身的特點，RTTC可以被定義為一個七元組：Tc=〈SId ，Tcl， Op ，Tcr， Pre，CLt，CLr〉。其中:SId是RTTC的有序標志集合；Tcl、 Tcr分別代表輸入值表示和預測輸出值表示；CLt和CLr分別代表輸入變量和預測輸出變量中所包含的時間約束值；Op代表它們之間的比較方式，根據前文中的假定5，這里的時間量之間的比較符號也可以是“≡”；Pre代表測試用例運行的前置條件，Pre:≡∑(WtPre)。

由于算法中用于構建RTTC的OT和CT已經具有時間約束，它可以在計算輸入和預測輸出變量的同時，計算輸入和預測輸出變量的時間約束量。從公理中構建RTTC的算法如下：

GenerationRealTimeTestCase

begin

 Give positive Nat SId

 Select axiom A =〈Ul， Op ，Ur， Pre〉∈ A

 while true do Tpre := calculate Time(Pre)

 Select CTi ∈ { CTi }

 For each variable of major type in Tcl ，Tcr ，Pre

Tcl，Tcr，Pre replace the variable with CTi

CLt := Tpre ；CLr:= Tpre + calculate Time(CTi)

 end for

 for each variable of other data types in Tcl ，Tcr ，Pre

if type of the variable is T

if T ∈ {Type of OTi }

select OTj ∈ {OTj} of data type T

else (Random Generate OTj of data type T )

end if

Tcl，Tcr，Pre replace the variable with OTi

CLt := Tpre ；CLr:= Tpre + calculate Time(OTi)

end if

 end for

 if result of Tcl is of major type and Op is ≡

 Select πo(Vok)∈{πo(Vo)}

Tcl :=πo(Vok) Tcr :=πo(Vok)replace major type input variable with Tcl ; Tcr

 end if

 return Tc =〈SId ，Tcl， Op ，Tcr ， Pre，CLt CLr〉

end

如前文假定d)所述，TRSL規約中，表達式可以理解為某個具體動作的程序化展現，基于規約的實時性測試的重點就是考察表達式實際執行獲得的輸出變量時間約束值與計算獲得的預測輸出變量的時間約束值是否相等。

在實際測試過程中，運行程序，輸入RTTC中給出的Tcl和CLt，將實際測得結果與Tcr和CLr進行比較，以判斷程序的正確性和實時性。

3 結束語

本文針對可信軟件實時性測試的需求，提出了一種基于TRSL的可信軟件實時性測試用例集生成方法。該方法是在傳統實時系統測試方法的基礎上展開的，有效解決了可信軟件實時性測試用例集生成難的問題。經驗證發現，與傳統方法相比，使用本方法生成的測試用例集不但定義更準確，而且更易于操作，具有很高的實用價值。

當然方法中還存在諸多不足，下一步的工作就將針對這些不足展開更深入的研究，如：OT和CT的長度k對測試精度影響很大，需要研究更為合理的設置方法；由于類型的不同，方法中表達式的運算時間量假定為定值或采用單一的計算方法可能不滿足實際需求，需要研究更為精確的時間量計算方法等。

參考文獻：

[1]劉克， 單志廣， 王戟，等.“可信軟件基礎研究”重大研究計劃綜述[J].中國科學基金， 2008， 22(3):145-151.

[2]MANDRIOLO D， MORASCA S， MORZENTI A. Generating test cases for real-time systems from logic specifications[J]. ACM Trans on Computer Systems， 1995， 13(4):365-398.

[3]CARDELL-OLIVER R， GLOVER T. A practical and complete algorithm for testing real-time systems[C]//Proc of the 5th International Symposium on Formal Techniques in Real-time and Fault-Tolerant Systems. London， UK: Springer-Verlag， 1998:251-261.

[4]陳偉， 薛云志， 趙琛，等. 一種基于時間自動機的實時系統測試方法[J]. 軟件學報， 2007， 18(1):62-73.

[5]The RAISE Language Group. The RAISE specification language[M]. [S.l.]:Prentice Hall， 1992.

[6]GEORGE C. Introducing time in RSL: a simple case study[R]. [S.l.]:UNU/IIST， 1998.

[7]LI Dan， BERNHARD K. Automatic test case generation for RAISE， Report No.273[R].[S.l.]:UNU/IIST， 2002.