鄧　輝，石竑松，張寶峰

（中國(guó)信息安全測(cè)評(píng)中心，北京 100085）

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

鄧輝，石竑松，張寶峰

（中國(guó)信息安全測(cè)評(píng)中心，北京 100085）

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

軟硬件功能測(cè)試；有限狀態(tài)機(jī)；Petri網(wǎng)；順序圖；等價(jià)性檢查

0　引 言

軟硬件功能測(cè)試是軟硬件開(kāi)發(fā)過(guò)程中的重要組成部分［1］。為發(fā)現(xiàn)軟硬件開(kāi)發(fā)可能帶來(lái)的錯(cuò)誤，測(cè)試根據(jù)軟硬件全生命周期中需求分析、設(shè)計(jì)、開(kāi)發(fā)等過(guò)程的文檔說(shuō)明，設(shè)計(jì)確定測(cè)試點(diǎn)、測(cè)試用例及測(cè)試方法，驗(yàn)證和確認(rèn)軟硬件功能，確定軟硬件功能的正確性和一致性，實(shí)現(xiàn)在軟硬件交付前，盡快及盡早發(fā)現(xiàn)軟硬件可能存在的與預(yù)定義、用戶(hù)需求等的不一致性，以降低改進(jìn)成本，減小因軟硬件開(kāi)發(fā)錯(cuò)誤造成的破壞，最終確保軟硬件的質(zhì)量［2-3］。

一般來(lái)說(shuō)，軟硬件測(cè)試有著規(guī)范的處理流程，包括測(cè)試計(jì)劃、方案以及規(guī)范的制訂，制訂后的實(shí)施和對(duì)實(shí)施所做的詳細(xì)記錄，以及基于記錄撰寫(xiě)測(cè)試報(bào)告。

具體來(lái)說(shuō)，軟硬件功能測(cè)試的內(nèi)容［4-5］包括：

（1）確認(rèn)軟硬件功能的正確性：一方面指確定軟硬件實(shí)現(xiàn)了預(yù)期的功能需求；另一方面指為達(dá)到此功能需求，軟硬件使用了正確的方式。

（2）確認(rèn)開(kāi)發(fā)過(guò)程的可行性：一旦軟硬件功能測(cè)試發(fā)現(xiàn)某一功能存在錯(cuò)誤，則說(shuō)明開(kāi)發(fā)過(guò)程存在問(wèn)題，因此需確認(rèn)軟硬件開(kāi)發(fā)過(guò)程是否可行，若不可行，需及時(shí)做出更改。從這個(gè)角度來(lái)講，軟硬件測(cè)試可促進(jìn)提高整個(gè)開(kāi)發(fā)過(guò)程的質(zhì)量。

近年來(lái)，功能測(cè)試作為提高軟硬件功能及開(kāi)發(fā)質(zhì)量的重要手段，在軟硬件開(kāi)發(fā)過(guò)程中越來(lái)越受到開(kāi)發(fā)人員的重視［6］。據(jù)統(tǒng)計(jì)，目前針對(duì)軟硬件功能測(cè)試的工作量已約占據(jù)整個(gè)軟硬件開(kāi)發(fā)工作量的40%左右，而測(cè)試成本占據(jù)軟硬件開(kāi)發(fā)成本的45%左右。但是，在已有的測(cè)試過(guò)程中，從開(kāi)發(fā)人員的角度出發(fā)，針對(duì)大部分測(cè)試點(diǎn)設(shè)計(jì)的測(cè)試用例均為抽樣方式。因此，存在測(cè)試用例設(shè)計(jì)的不完整或者說(shuō)是存在完備性問(wèn)題，使得功能測(cè)試的全過(guò)程可以發(fā)現(xiàn)軟硬件在功能上存在的錯(cuò)誤，而不能確保軟硬件功能完全沒(méi)有錯(cuò)誤。這也是大多數(shù)軟硬件在交付后投入使用時(shí)會(huì)出現(xiàn)很多bug的主要原因。因此，針對(duì)軟硬件設(shè)計(jì)完整的測(cè)試點(diǎn)及測(cè)試用例生成方法是開(kāi)發(fā)人員需要解決的問(wèn)題［7-8］。

對(duì)于該問(wèn)題，研究人員已經(jīng)投入了大量時(shí)間和精力，企圖從理論角度解決完備性問(wèn)題。對(duì)于軟件功能測(cè)試來(lái)說(shuō)，目前已有的測(cè)試點(diǎn)主要分為單元測(cè)試、集成測(cè)試以及系統(tǒng)測(cè)試［9-10］。單元測(cè)試指在軟件開(kāi)發(fā)過(guò)程中，將軟件的每一個(gè)最小單位模塊作為測(cè)試點(diǎn)，設(shè)計(jì)測(cè)試用例；集成測(cè)試指將已測(cè)試的模塊進(jìn)行組裝，將每一個(gè)組裝作為一個(gè)測(cè)試點(diǎn)，設(shè)計(jì)測(cè)試用例；而系統(tǒng)測(cè)試指將整個(gè)軟件作為一個(gè)測(cè)試點(diǎn)，進(jìn)行黑盒測(cè)試。

設(shè)置測(cè)試點(diǎn)后，對(duì)應(yīng)已有的測(cè)試用例生成方法主要包括因果圖分析法、邊界值分析法、等價(jià)類(lèi)劃分法以及錯(cuò)誤推測(cè)法。其中，因果圖分析法指利用圖解法分析輸入的各種組合情況設(shè)計(jì)測(cè)試用例；邊界分析法指通過(guò)輸入和輸出的邊界值設(shè)計(jì)測(cè)試用例；等價(jià)類(lèi)劃分法指為減低測(cè)試數(shù)目同時(shí)實(shí)現(xiàn)合理覆蓋，通過(guò)選擇適當(dāng)?shù)臄?shù)據(jù)子集來(lái)代表整個(gè)數(shù)據(jù)集來(lái)設(shè)置測(cè)試用例；錯(cuò)誤推測(cè)法指根據(jù)經(jīng)驗(yàn)和直覺(jué)推測(cè)程序中可能存在的各種錯(cuò)誤，并針對(duì)性地編寫(xiě)檢查錯(cuò)誤的測(cè)試用例。這四種方法均為黑盒測(cè)試，對(duì)于軟硬件來(lái)說(shuō)，均不利于實(shí)現(xiàn)問(wèn)題的有效定位。

為建立通用的軟硬件測(cè)試用例生成方法，本文首先抽取有限狀態(tài)機(jī)、Petri網(wǎng)、順序圖的優(yōu)點(diǎn)混合后，對(duì)軟硬件功能的動(dòng)靜態(tài)特征及其功能屬性進(jìn)行抽象建模，并進(jìn)行特征優(yōu)化，為測(cè)試用例生成提供基礎(chǔ)框架。然后，分別將軟硬件每一個(gè)功能入口作為測(cè)試點(diǎn)。利用軟硬件功能策略圖分別描述該測(cè)試點(diǎn)在軟硬件模型及其功能屬性模型中的功能特征。如果后者蘊(yùn)含前者，則證明功能屬性被滿(mǎn)足，意味該項(xiàng)功能測(cè)試通過(guò)。

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

在半形式化方法中，有限狀態(tài)圖著重刻畫(huà)對(duì)象的狀態(tài)以及遷移關(guān)系，刻畫(huà)方式直觀且可讀性高，但未對(duì)遷移關(guān)系進(jìn)行細(xì)化。Petri網(wǎng)對(duì)遷移關(guān)系的順序、并發(fā)、沖突進(jìn)行了詳細(xì)定義，但引入符號(hào)過(guò)多，操作復(fù)雜度較大。為解決此問(wèn)題，本節(jié)將以有限狀態(tài)圖作為軟硬件功能基礎(chǔ)刻畫(huà)框架，并將Petri網(wǎng)的遷移關(guān)系分類(lèi)添加到有限狀態(tài)圖中。

對(duì)于軟硬件來(lái)說(shuō)，外界與其功能進(jìn)行交互時(shí)均通過(guò)功能入口。功能入口可以是一個(gè)函數(shù)，稱(chēng)為邏輯入口；也可以是一個(gè)硬件入口，如一個(gè)硬件引腳，稱(chēng)為物理入口。其中，軟件功能入口均為邏輯入口；硬件功能入口包括邏輯入口（如命令和函數(shù)）和物理入口（如硬件表面等）?；诠δ苋肟诘姆诸?lèi)，軟硬件功能正確，表明外界通過(guò)功能入口所執(zhí)行的功能策略正確。某項(xiàng)具體功能策略的執(zhí)行，可描述為處于某一狀態(tài)下，基于某種正常的入口使用方式成功使用該入口，可執(zhí)行此項(xiàng)功能，觸發(fā)一個(gè)正確的入口遷移。

為描述此過(guò)程，對(duì)有限狀態(tài)圖、Petri網(wǎng)、順序圖的狀態(tài)及遷移關(guān)系進(jìn)行重新定義，稱(chēng)為軟硬件功能策略圖，如圖1所示。

軟硬件功能策略圖是四元組（S，R，U，A）：S是有限狀態(tài)的集合，用圓形表示，對(duì)應(yīng)入口使用方式所涉及的參數(shù)；R是有限功能入口的集合，用圓形方框表示；U是有限功能入口使用方式的集合，用指向R的箭頭表示；A是有限功能遷移的集合，用R指出的箭頭表示；功能遷移指通過(guò)正常使用方式，使用功能入口后觸發(fā)的一個(gè)入口動(dòng)作遷移。

圖1中，重定義的操作符號(hào)包括：

（1）豎線(xiàn)表示并發(fā)遷移的分叉連接符，或者合并遷移的合并連接符；

（2）狀態(tài)下的矩形條表示此狀態(tài)將先后觸發(fā)多功能入口；入口下虛線(xiàn)表示該入口的生命線(xiàn)；生命線(xiàn)上的矩形條表示通過(guò)此入口觸發(fā)的一個(gè)動(dòng)作；多個(gè)入口的生命線(xiàn)上的矩形條由上往下代表動(dòng)作觸發(fā)的先后順序；

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

圖1　軟硬件功能策略

下面詳細(xì)論述四種遷移：順序遷移、并發(fā)遷移、沖突遷移和合并遷移。

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

圖2　順序遷移

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

圖3　并發(fā)遷移

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

圖4　沖突遷移

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

圖5　合并遷移

2　模型結(jié)構(gòu)化簡(jiǎn)

在描述并發(fā)、沖突及合并遷移時(shí)發(fā)現(xiàn)，假設(shè)觸發(fā)同一個(gè)遷移的狀態(tài)和功能入口使用方式相同，則可將它們進(jìn)行合并，化簡(jiǎn)軟硬件功能策略圖的整體結(jié)構(gòu)。如果假設(shè)成立，則約簡(jiǎn)到復(fù)雜的使用方式及功能入口，圖1可能存在如下化簡(jiǎn)。

（1）并發(fā)遷移結(jié)構(gòu)的化簡(jiǎn)，如圖6所示。

圖6　并發(fā)遷移結(jié)構(gòu)化簡(jiǎn)

（2）沖突遷移結(jié)構(gòu)的化簡(jiǎn)，如圖7所示。

圖7　沖突遷移結(jié)構(gòu)化簡(jiǎn)

（3）合并遷移結(jié)構(gòu)的化簡(jiǎn)，如圖8所示。

圖8　合并遷移結(jié)構(gòu)化簡(jiǎn)

于是，圖1最終可化簡(jiǎn)為圖9。

圖9　功能策略圖的化簡(jiǎn)

3　軟硬件功能測(cè)試用例生成

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

圖10　一致性驗(yàn)證框架

在實(shí)現(xiàn)功能需求與設(shè)計(jì)的一致性分析驗(yàn)證后，需要驗(yàn)證軟硬件確實(shí)按照設(shè)計(jì)進(jìn)行了安全實(shí)現(xiàn)。此時(shí)，需證明下述兩個(gè)要素均得到了滿(mǎn)足：

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

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

為證明滿(mǎn)足了上述兩個(gè)要素，軟硬件功能實(shí)現(xiàn)正確的測(cè)試用例的生成及驗(yàn)證步驟。軟硬件功能策略圖中的每一條遷移路徑，均對(duì)應(yīng)一個(gè)測(cè)試用例。具體的測(cè)試用例可設(shè)計(jì)為，首先基于軟硬件功能策略圖等同建模軟硬件功能需求，然后基于等價(jià)性檢查驗(yàn)證軟硬件功能需求模型，其均等價(jià)對(duì)應(yīng)一個(gè)測(cè)試用例的遷移路徑。如果驗(yàn)證通過(guò)，則證明軟硬件功能實(shí)現(xiàn)正確。驗(yàn)證基本原理圖將在下一節(jié)實(shí)例分析中給出。

4　實(shí)例

以智能卡產(chǎn)品為例，模式控制是其典型的安全功能。該功能要求產(chǎn)品測(cè)試模式、BOOT模式、COS模式之間僅為單向轉(zhuǎn)換關(guān)系，以確保產(chǎn)品在功能測(cè)試結(jié)束后，下級(jí)模式用戶(hù)使用時(shí)無(wú)法再進(jìn)入上級(jí)模式修改產(chǎn)品安全配置。COS模式無(wú)法調(diào)用正常的操作BOOT模式的指令接口返回BOOT模式，但BOOT模式常為COS模式用戶(hù)提供部分函數(shù)功能入口，使COS模式可再次返回BOOT模式進(jìn)行相關(guān)安全操作。

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

圖11　功能需求半形式化

具體設(shè)計(jì)的半形式化描述，如圖12所示。

圖12　功能設(shè)計(jì)半形式化

通過(guò)分析發(fā)現(xiàn)，圖11與圖12策略相同?；趫D12獲得此功能策略正確性測(cè)試用例，如圖13所示。

圖13　功能測(cè)試用例生成

5　結(jié) 語(yǔ)

本文提出了一種軟硬件功能測(cè)試用例生成的半形式化框架。該框架具備通用性，適用于所有的軟硬件，實(shí)現(xiàn)了軟硬件功能策略描述。未來(lái)將尋求形式化的方法，表征攻擊入口的使用方式及觸發(fā)遷移，以實(shí)現(xiàn)軟硬件功能正確性的形式化推導(dǎo)。

［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］ 孫莉.基于構(gòu)件的軟件測(cè)試中測(cè)試用例分配優(yōu)化研究［J］.通信技術(shù)，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］ 楊波，吳際，徐珞等.一種軟件測(cè)試需求建模及測(cè)試用例生成方法［J］.計(jì)算機(jī)學(xué)報(bào)，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鏈的軟件自適應(yīng)測(cè)試策略［J］.計(jì)算機(jī)研究與發(fā)展，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

國(guó)家自然科學(xué)基金（No.61472448）

鄧 輝（1985—），女，博士，助理研究員，主要研究方向?yàn)樾畔踩?/p>

石竑松（1978—），男，博士，副研究員，主要研究方向?yàn)樾畔踩?/p>

張寶峰（1983—），男，碩士，副研究員，主要研究方向?yàn)樾畔踩?/p>