軟硬件功能測試用例半形式化生成方法*

鄧 輝，石竑松，張寶峰

（中國信息安全測評中心，北京 100085）

軟硬件功能測試用例半形式化生成方法*

鄧 輝，石竑松，張寶峰

（中國信息安全測評中心，北京 100085）

功能測試旨在保證軟硬件正確性，降低生產成本。已有的功能測試均為黑盒測試，無法最大化地發現功能正確性問題。而半形式化方法可為最大化分析、驗證軟硬件正確性提供框架。因此，圍繞功能入口，混合有限狀態機、Petri網、順序圖，共同建模軟硬件動靜態特征及其功能屬性，并建立模型簡化規則。模型由功能入口使用方式、功能入口、功能入口觸發遷移三部分組成，覆蓋所有功能入口模擬測試場景，并最大化生成測試用例。最終，基于模型等價性，檢查實現功能測試的描述。

軟硬件功能測試；有限狀態機；Petri網；順序圖；等價性檢查

0　引 言

軟硬件功能測試是軟硬件開發過程中的重要組成部分［1］。為發現軟硬件開發可能帶來的錯誤，測試根據軟硬件全生命周期中需求分析、設計、開發等過程的文檔說明，設計確定測試點、測試用例及測試方法，驗證和確認軟硬件功能，確定軟硬件功能的正確性和一致性，實現在軟硬件交付前，盡快及盡早發現軟硬件可能存在的與預定義、用戶需求等的不一致性，以降低改進成本，減小因軟硬件開發錯誤造成的破壞，最終確保軟硬件的質量［2-3］。

一般來說，軟硬件測試有著規范的處理流程，包括測試計劃、方案以及規范的制訂，制訂后的實施和對實施所做的詳細記錄，以及基于記錄撰寫測試報告。

具體來說，軟硬件功能測試的內容［4-5］包括：

（1）確認軟硬件功能的正確性：一方面指確定軟硬件實現了預期的功能需求；另一方面指為達到此功能需求，軟硬件使用了正確的方式。

（2）確認開發過程的可行性：一旦軟硬件功能測試發現某一功能存在錯誤，則說明開發過程存在問題，因此需確認軟硬件開發過程是否可行，若不可行，需及時做出更改。從這個角度來講，軟硬件測試可促進提高整個開發過程的質量。

近年來，功能測試作為提高軟硬件功能及開發質量的重要手段，在軟硬件開發過程中越來越受到開發人員的重視［6］。據統計，目前針對軟硬件功能測試的工作量已約占據整個軟硬件開發工作量的40%左右，而測試成本占據軟硬件開發成本的45%左右。但是，在已有的測試過程中，從開發人員的角度出發，針對大部分測試點設計的測試用例均為抽樣方式。因此，存在測試用例設計的不完整或者說是存在完備性問題，使得功能測試的全過程可以發現軟硬件在功能上存在的錯誤，而不能確保軟硬件功能完全沒有錯誤。這也是大多數軟硬件在交付后投入使用時會出現很多bug的主要原因。因此，針對軟硬件設計完整的測試點及測試用例生成方法是開發人員需要解決的問題［7-8］。

對于該問題，研究人員已經投入了大量時間和精力，企圖從理論角度解決完備性問題。對于軟件功能測試來說，目前已有的測試點主要分為單元測試、集成測試以及系統測試［9-10］。單元測試指在軟件開發過程中，將軟件的每一個最小單位模塊作為測試點，設計測試用例；集成測試指將已測試的模塊進行組裝，將每一個組裝作為一個測試點，設計測試用例；而系統測試指將整個軟件作為一個測試點，進行黑盒測試。

設置測試點后，對應已有的測試用例生成方法主要包括因果圖分析法、邊界值分析法、等價類劃分法以及錯誤推測法。其中，因果圖分析法指利用圖解法分析輸入的各種組合情況設計測試用例；邊界分析法指通過輸入和輸出的邊界值設計測試用例；等價類劃分法指為減低測試數目同時實現合理覆蓋，通過選擇適當的數據子集來代表整個數據集來設置測試用例；錯誤推測法指根據經驗和直覺推測程序中可能存在的各種錯誤，并針對性地編寫檢查錯誤的測試用例。這四種方法均為黑盒測試，對于軟硬件來說，均不利于實現問題的有效定位。

為建立通用的軟硬件測試用例生成方法，本文首先抽取有限狀態機、Petri網、順序圖的優點混合后，對軟硬件功能的動靜態特征及其功能屬性進行抽象建模，并進行特征優化，為測試用例生成提供基礎框架。然后，分別將軟硬件每一個功能入口作為測試點。利用軟硬件功能策略圖分別描述該測試點在軟硬件模型及其功能屬性模型中的功能特征。如果后者蘊含前者，則證明功能屬性被滿足，意味該項功能測試通過。

1　軟硬件功能策略半形式化建模

在半形式化方法中，有限狀態圖著重刻畫對象的狀態以及遷移關系，刻畫方式直觀且可讀性高，但未對遷移關系進行細化。Petri網對遷移關系的順序、并發、沖突進行了詳細定義，但引入符號過多，操作復雜度較大。為解決此問題，本節將以有限狀態圖作為軟硬件功能基礎刻畫框架，并將Petri網的遷移關系分類添加到有限狀態圖中。

對于軟硬件來說，外界與其功能進行交互時均通過功能入口。功能入口可以是一個函數，稱為邏輯入口；也可以是一個硬件入口，如一個硬件引腳，稱為物理入口。其中，軟件功能入口均為邏輯入口；硬件功能入口包括邏輯入口（如命令和函數）和物理入口（如硬件表面等）。基于功能入口的分類，軟硬件功能正確，表明外界通過功能入口所執行的功能策略正確。某項具體功能策略的執行，可描述為處于某一狀態下，基于某種正常的入口使用方式成功使用該入口，可執行此項功能，觸發一個正確的入口遷移。

為描述此過程，對有限狀態圖、Petri網、順序圖的狀態及遷移關系進行重新定義，稱為軟硬件功能策略圖，如圖1所示。

軟硬件功能策略圖是四元組（S，R，U，A）：S是有限狀態的集合，用圓形表示，對應入口使用方式所涉及的參數；R是有限功能入口的集合，用圓形方框表示；U是有限功能入口使用方式的集合，用指向R的箭頭表示；A是有限功能遷移的集合，用R指出的箭頭表示；功能遷移指通過正常使用方式，使用功能入口后觸發的一個入口動作遷移。

圖1中，重定義的操作符號包括：

（1）豎線表示并發遷移的分叉連接符，或者合并遷移的合并連接符；

（2）狀態下的矩形條表示此狀態將先后觸發多功能入口；入口下虛線表示該入口的生命線；生命線上的矩形條表示通過此入口觸發的一個動作；多個入口的生命線上的矩形條由上往下代表動作觸發的先后順序；

（3）每一條遷移路徑均代表軟硬件的一條功能策略。

圖1　軟硬件功能策略

下面詳細論述四種遷移：順序遷移、并發遷移、沖突遷移和合并遷移。

（1）順序遷移，如圖2所示。此功能策略表示軟硬件在狀態S1下，基于使用方式U1使用該策略入口R1，執行遷移A1+S5。

圖2　順序遷移

（2）并發遷移，如圖3所示。此功能策略表示軟硬件在狀態S2下，基于使用方式U2使用該策略入口R2，執行并發遷移A3+S3或A4+S4。

圖3　并發遷移

（3）沖突遷移，如圖4所示。此功能策略表示軟硬件在狀態S1下，基于使用方式U2使用該策略入口R2，可能執行遷移A3+S3或A4+S4或A5+S5。此過程造成非確定性，可能引發沖突。

圖4　沖突遷移

（4）合并遷移，如圖5所示。該功能策略表示軟硬件在狀態S1下，基于使用方式U2使用該策略入口R2，或基于使用方式U3使用該策略入口R3，執行遷移A5+S5；同時，在狀態S2下，基于使用方式U4使用策略入口R3，同樣可執行遷移A5+S5。

圖5　合并遷移

2　模型結構化簡

在描述并發、沖突及合并遷移時發現，假設觸發同一個遷移的狀態和功能入口使用方式相同，則可將它們進行合并，化簡軟硬件功能策略圖的整體結構。如果假設成立，則約簡到復雜的使用方式及功能入口，圖1可能存在如下化簡。

（1）并發遷移結構的化簡，如圖6所示。

圖6　并發遷移結構化簡

（2）沖突遷移結構的化簡，如圖7所示。

圖7　沖突遷移結構化簡

（3）合并遷移結構的化簡，如圖8所示。

圖8　合并遷移結構化簡

于是，圖1最終可化簡為圖9。

圖9　功能策略圖的化簡

3　軟硬件功能測試用例生成

軟硬件功能策略圖完整描述了為實現軟硬件功能，具體設計和實現的策略，同時實現了策略的完整梳理。其中，功能入口是執行該策略的媒介。在確保軟硬件功能完整性描述的前提下，若要證明軟硬件功能的正確性，需首先基于本文建立的半形式化方法描述軟硬件功能策略需求及具體實現，然后判斷此兩模型間是否存在狀態一一映射關系，若存在，則表明功能設計正確，過程如圖10所示。

圖10　一致性驗證框架

在實現功能需求與設計的一致性分析驗證后，需要驗證軟硬件確實按照設計進行了安全實現。此時，需證明下述兩個要素均得到了滿足：

（1）功能入口使用方式是正確的；

（2）由功能入口觸發的功能遷移是正確的。

為證明滿足了上述兩個要素，軟硬件功能實現正確的測試用例的生成及驗證步驟。軟硬件功能策略圖中的每一條遷移路徑，均對應一個測試用例。具體的測試用例可設計為，首先基于軟硬件功能策略圖等同建模軟硬件功能需求，然后基于等價性檢查驗證軟硬件功能需求模型，其均等價對應一個測試用例的遷移路徑。如果驗證通過，則證明軟硬件功能實現正確。驗證基本原理圖將在下一節實例分析中給出。

4　實例

以智能卡產品為例，模式控制是其典型的安全功能。該功能要求產品測試模式、BOOT模式、COS模式之間僅為單向轉換關系，以確保產品在功能測試結束后，下級模式用戶使用時無法再進入上級模式修改產品安全配置。COS模式無法調用正常的操作BOOT模式的指令接口返回BOOT模式，但BOOT模式常為COS模式用戶提供部分函數功能入口，使COS模式可再次返回BOOT模式進行相關安全操作。

此過程涉及的功能需求基于本文的混合半形式化方法建模，可描述為如圖11所示。

圖11　功能需求半形式化

具體設計的半形式化描述，如圖12所示。

圖12　功能設計半形式化

通過分析發現，圖11與圖12策略相同。基于圖12獲得此功能策略正確性測試用例，如圖13所示。

圖13　功能測試用例生成

5　結 語

本文提出了一種軟硬件功能測試用例生成的半形式化框架。該框架具備通用性，適用于所有的軟硬件，實現了軟硬件功能策略描述。未來將尋求形式化的方法，表征攻擊入口的使用方式及觸發遷移，以實現軟硬件功能正確性的形式化推導。

［1］ Swain R，Panthi V，Behera P K，et al.Automatic Test Case Generation from UML State Chart Diagram［J］.International Journal of Computer Applications，2012，42（07）：26-36.

［2］ Wang Y，Zheng M.Test Case Generation from UML Models［C］.45th Annual Midwest Instruction and Computing Sympos-ium，2012.

［3］ Francisco M A，Castro L M.Automatic Generation of Test Models and Properties from UML Models with OCL Constraints［C］.Proceedings of the 12th Workshop on OCL and Textual Modelling，2012：49-54.

［4］ Hemmati H，Arcuri A，Briand L.Achieving Scalable Model-based Testing through Test Case Diversity［J］. ACM Transactions on Software Engineering and Methodology，2013，22（01）：6.

［5］ Shirole M，Kumar R.UML Behavioral Model based Test Case Generation：A Survey［J］.ACM SIGSOFT Software Engineering Notes，2013，38（04）：1-13.

［6］ 孫莉.基于構件的軟件測試中測試用例分配優化研究［J］.通信技術，2008，41（10）：193-195. SUN Li.Optimization of Test Case Allocation in Component-based Software Testing［J］.Communications Technology，2008，41（10）：193-195.

［7］ Jorgensen P C.Software Testing：A Craftsman's Approach［M］. Boca Raton：CRC press，2013.

［8］ ?ivkovi? A，Rozman I，Heri?ko M.Automated Software Size Estimation based on Function Points Using UML models［J］. Information and Software Technology，2005，47（13）：881-890.

［9］ 楊波，吳際，徐珞等.一種軟件測試需求建模及測試用例生成方法［J］.計算機學報，2014，37（03）：522-538. YANG Bo，WU Ji，XU Luo，et al.An Approuch of Modeling Software Testing Requirements and Generating Test Case［J］. Chinese Journal of Computers，2014，37（03）：522-538.

［10］ 包曉安，姚瀾，張娜等.基于受控Markov鏈的軟件自適應測試策略［J］.計算機研究與發展，2012，49（06）：1332-1338. BAO Xiao-an，YAO Lan，ZHANG Na，et al.Adaptive Software Testing based on Controlled Markov Chain［J］.Journal of Computer Research and Development，2012，49（06）：1332-1338.

Software and Hardware Functional Test Case based on Semi-formal Generating Method

DENG Hui， SHI Hong-song， ZHANG Bao-feng
（China Information Technology Security Evaluation Center， Beijing 100085， China）

Functional test is for the purpose of ensuring the correctness and reducing the cost of software and hardware. The existing function tests are usually the so-called balck-box test， which could not find out all problems in correctness verification. Semi-formal method could provide a framework to deal with this problem. This paper， around functional interface， describes the dynamic and static characteristics of software and hardware based on finite-state machine， Petri net and sequence diagram. And the description model containing interface， behavior and action of the interface is also established. Then， a depth traversal is applied to covering all of the test scenarios around interface so that the maximal test cases can be acquired. Finally， based on equivalence of the model， The description of functional test implementation is examined.

software and hardware functional test； finite-state machine； petri net； sequence diagram；equivalence verification

National Natural Science Foundation of China（No.61472448）

TP311.52

A

1002-0802（2016）-10-1364-05

10.3969/j.issn.1002-0802.2016.10.019

2016-06-07；

2016-09-23

data：2016-06-07；Revised data：2016-09-23

國家自然科學基金（No.61472448）

鄧 輝（1985—），女，博士，助理研究員，主要研究方向為信息安全；

石竑松（1978—），男，博士，副研究員，主要研究方向為信息安全；

張寶峰（1983—），男，碩士，副研究員，主要研究方向為信息安全。