面向安全苛求軟件的測試用例自動生成
2009-01-01 00:00:00章文婷徐中偉喻剛
計算機應用研究 2009年1期
（同濟大學 電子與信息工程學院 信通系， 上海 201804）
摘 要：測試用例的自動生成是驗證安全苛求軟件最關鍵的技術問題，然而目前的研究并沒有充分考慮安全苛求軟件的安全性需求，為此提出一種應用安全覆蓋準則的安全苛求軟件的測試用例自動生成策略，將該策略應用于鐵路車站計算機連鎖軟件，并與全節點覆蓋準則進行了比較。結果表明該策略對關鍵變遷有更高的安全性保證。
關鍵詞：安全苛求軟件； 測試用例自動生成； 安全覆蓋準則
中圖分類號：TP311.56 文獻標志碼：A
文章編號：10013695(2009)01014003
Automated test data generation for safety critical software
ZHANG Wenting， XU Zhongwei， YU Gang
（Dept. ofInformation Communication， School of Electronics Information Engineering， Tongji University， Shanghai 201804， China）
Abstract:Automated test data generation is the most crucial technology to evaluate safetycritical software. However， the current thesis are not fully considered the safety requirement of safetycritical software， therefore the paper presented an automated test data generation strategy for safetycritical software using safety coverage criteria. At last applied the strategy to the railway station computer interlocking software. Compared with all nodes coverage criteria， it shows that has higher safety guarantee to critical transition.
Key words：safety critical software; automated test data generation; safety coverage criteria
軟件應用的日趨廣泛， 加深了社會和經濟對計算機的依賴，但軟件故障時常會給人們的生活帶來不便， 甚至不安。特別是一些軟件， 其行為直接關系到人們的生命安全、大宗財產的損失和嚴重的環境破壞。這些軟件就是通常所說的安全苛求軟件[1]。如何保障這些軟件的質量，防止災難性事故的出現，已成為一個刻不容緩的研究課題。
軟件測試是軟件生產中必不可少的質量保障手段。尤其是對于高可靠、高安全的安全苛求軟件，更需要對它進行測試以盡可能多地發現程序中的缺陷。基于規格說明的測試從軟件的規格說明推導測試用例。目前的研究主要對功能性需求規格進行建模，研究人員提出了各種覆蓋準則覆蓋狀態圖中的所有功能。然而對于安全苛求軟件，僅僅覆蓋軟件功能是不充分的。因此本文提出了一種應用安全覆蓋準則的安全苛求軟件的測試用例生成策略：采用測試用例自動生成算法，生成覆蓋所有節點、覆蓋導致軟件失效的關鍵變遷中防護函數的謂詞公式的遷移序列，從而得到測試用例。
1 從形式規格說明產生測試用例的現狀分析
軟件的需求規格說明分為兩類，即功能性需求規格和安全性需求規格。功能性需求規格常常注重各個構件所能完成的功能；安全性需求規格側重各個構件之間的約束關系。以鐵路連鎖軟件為例，它由信號機、道岔和區段這幾個構件組成。圖1體現了兩種需求規格間的差異。
由圖1可以看到，功能性需求規格體現了單個構件的功能，描述了系統的正確行為，如信號機的開放和關閉功能、道岔的轉動和鎖閉功能，以及區段的占用和鎖閉功能。但是如果某一區段處于占用狀態或道岔沒有鎖閉，這樣的危險組合下建立進路可能會引發撞車、擠岔等嚴重事故，因此必須關閉信號機。安全需求規格就定義了這些構件之間的制約規則，并要求屏蔽那些危險組合，由故障導向安全。
目前從形式規格說明產生測試用例的方法都是針對軟件的功能性需求規格進行建模，使用的覆蓋準則只是考慮覆蓋狀態圖中的所有節點或所有謂詞公式。例如文獻[2]利用基于有限狀態機的經典測試U方法來自動生成測試輸入序列，其測試序列覆蓋每個狀態遷移，當其測試覆蓋準則僅僅是最基本的狀態覆蓋準則；文獻[3]根據UML狀態圖對被測試的對象行為或系統行為建模，然后按照不同的充分性測試準則分別生成測試用例，造成測試用例過于龐大，浪費了過多的時間和精力。
對于安全苛求軟件的測試，關鍵是消除并控制軟件出現危險或發生意外事故，所以上述方法考慮功能性需求是不充分的，必須對安全苛求軟件的安全性需求規格進行建模。有色Petri網[4](colored Petri net，CPN)提供了一種精確的、一致的、易于被機器處理的符號來描述需求規格，相較于有限狀態機和UML狀態圖，它簡化了大型實際系統模型的復雜程度，更好地描述了模型的并發、沖突狀況。與功能性需求建模不同的是，形式化安全性需求應該著重描述構件間的約束規則及系統發生失效的行為和結果。鑒于安全性需求和功能性需求的不同，測試用例的充分性不再體現在覆蓋所有功能上，而是需要完全覆蓋各種可能的失效情況，所以上述方法中的覆蓋準則不再適用。本文在文獻[3]和基本測試覆蓋準則的基礎上，提出了一種新的適用于安全苛求軟件的測試覆蓋準則——安全覆蓋準則；然后采用有色Petri網形式化安全需求規格說明，根據此覆蓋準則，通過測試用例自動生成算法生成覆蓋所有庫所和變遷的遷移序列，并在導致軟件失效的關鍵變遷上對遷移序列進行全謂詞公式覆蓋擴展；最后從遷移序列得到測試用例。
2 安全覆蓋準則
安全性需求的重要部分在于軟件如何以安全的失效方法以及失效可以容許到何種程度的規范約束，因此適用于功能性需求規格的覆蓋準則只考慮全面覆蓋狀態圖中的所有節點是不足的，必須充分挖掘導致軟件失效并引發嚴重事故的所有測試條件組合。根據以上思路，本文提出了安全覆蓋準則。定義安全覆蓋準則之前，先引入關鍵變遷的概念。
定義1 給定一個t，如果t(v=1)，則稱t為關鍵變遷。其中：t表示Petri網模型中的變遷；v表示Petri網模型中的防護函數。
根據關鍵變遷的定義，可以看到它對應需求規格說明模型中存在判斷且判斷為假的部分，而在安全苛求軟件中，它可能會引發或產生嚴重危害性事故。安全覆蓋準則定義如下：
定義2 給定一個S，其滿足條件：a)p∈P，pS；b)t∈T，tS;c)v∈V，(v∧v)S，則稱S符合安全覆蓋準則。其中：S表示測試用例集；p表示Petri網模型中的庫所；t表示Petri網模型中的變遷；v表示Petri網模型中的防護函數。安全覆蓋準則說明測試用例集應該使模型中的每一個庫所至少被訪問一次，每一個變遷至少被激活一次，且使Petri網模型中關鍵變遷的防護函數v的每一個主要謂詞P取假各一次（次要謂詞都為真）。防護函數的謂詞公式中凡是要測試的謂詞都應該分別充當一次主要謂詞。對于一個主要謂詞分別取假一次，將分別對應一個測試用例的產生。可見滿足安全覆蓋準則的這些測試用例遍歷了模型中所有的節點，并且完全包含了可能導致危害性事故的變遷的各種謂詞組合。
3 應用安全覆蓋準則的安全苛求軟件測試用例自動生成策略
該策略的基本思路是首先對安全苛求軟件進行安全需求分析，確定系統導致事故的狀態，然后利用有色Petri網對安全需求規格說明進行建模。根據安全覆蓋準則，利用測試用例自動生成算法搜索得到測試用例，產生的測試用例不僅可以覆蓋測試對象的所有狀態和變遷，能夠覆蓋關鍵變遷中的所有謂詞公式。整個過程如圖2所示。
本文采用的是測試用例自動生成算法來生成測試用例。圖3是具體的算法流程圖。
二維表的結構如表1所示。其表的行、列分別表示目標庫所、源庫所。行和列的交叉點表示從源庫所到目標庫所經歷的變遷。在關鍵變遷處加入防護函數。
上述算法遍歷了有色Petri模型并產生了遷移序列，將這些序列用于產生測試用例。每個序列描述了從初始狀態到完成狀態所經歷的所有變遷。比如序列P1、T1、P2，測試的輸入條件是：源狀態為P1，觸發事件為T1，監視條件為真，期望結果是P2。這樣一個序列將產生一個測試用例。
定義3 安全苛求軟件測試案例T可以用一個三元組〈S0；E；S〉表示。其中：E＝e^v。T有一個初始狀態S0；E表示變遷事件和變遷上防護函數的合取式；S是預期狀態。
上述測試用例集對每一個遷移序列進行了測試，顯然，由上述策略生成的測試集覆蓋了有色Petri模型的所有狀態和變遷，并且在關鍵變遷處覆蓋了所有謂詞取值組合，將有限的資源和時間立足在導致軟件失效之處。
4 應用實例
鐵路連鎖系統軟件，即鐵路車站控制與防護系統的安全軟件。它是用于控制和指揮鐵路列車運行、保障鐵路行車安全的實時控制軟件。它直接控制著整個鐵路信號系統，對提高運輸效率，保證客貨安全運輸起著舉足輕重的作用。與其他眾多大型軟件一樣，鐵路連鎖系統的軟件在開發過程中，即使程序設計工作進行得非常細致周密，也難免存在缺陷，可能使程序運行時產生危險性輸出。這里就以鐵路車站計算機連鎖系統的基本進路建立功能來說明測試用例生成過程。
對于連鎖軟件中的基本進路建立，需要滿足以下主要連鎖安全條件：
a)進路上的所有軌道區段空閑并且解鎖;
b)超限絕緣安全條件檢查正確;
c)進路上的道岔和防護道岔被鎖閉;
d)進路的敵對進路未建立。
接下來對基本進路建立的安全需求進行建模。圖4是基本進路建立的有色Petri網模型。
有色Petri網模型的庫所集如表2所示。
對于P中的各個庫所C(p)=route，route定義為一個記錄，記錄組成如下所示：
其中：ID表示進路編號；Ai和Bi分別代表始端按鈕和終端按鈕；switch1～switch10表示進路上的10個道岔（設最大數為10）；opsig1～opsig10表示進路的10個敵對信號（設最大數為10）；section1～section10表示進路上的10個區段（設最大數為10）；cxjy1～cxjy10表示為進路上的10個超限絕緣條件（設最大數為10）。
針對基本進路建立問題，分別使用全節點覆蓋準則和安全覆蓋準則生成測試用例。實驗結果如圖6所示。
從圖6中可以看到，安全覆蓋準則應用于關鍵變遷的測試用例比例遠遠高于全節點覆蓋準則。可見對于可能造成安全苛求軟件失效的關鍵變遷處安全覆蓋準則擁有更高的覆蓋率，因此它比全節點覆蓋準則具有更好的安全性保證。
6 結束語
本文提出的針對安全苛求軟件的測試用例生成策略，應用安全覆蓋準則自動生成測試用例。它是一種自動黑盒測試方法，它使從測試規格說明產生測試用例的過程自動化，減少了軟件測試的復雜度。實驗表明，它對于安全苛求軟件具有更好的安全性保證。今后的研究工作將放在開發出一個高效、實用的測試用例自動生成工具上。
參考文獻：
[1]ISAKSEN U， BOWEN J P， NISSANKE N. System and software safety in critical systems[EB/OL]. （1996）[20080527].http://citeseer.ist.psu.edu/isaksen96system.html.
[2]年曉玲. 基于擴展有限狀態機軟件測試用例自動生成的研究[D].成都：西南交通大學， 2005.
[3]占學德. 基于UML statecharts測試方法的研究[D].上海：上海大學，2005.
［4］JENSEN K. Colored Petri nets:basic concepts， analysis methods and practical use[M]. 2rd ed. Berlin， New York: SpringerVerlag， 1995.
[5]DICK J， FAIVRE A. Automating the generation and sequencing of test cases from modelbased specification[C]//Proc of the 1st International Symposium of Formal Methods Europe on IndustrialStrength Formal Methods. London:SpringerVerlag， 1993:268284.
