Kaputt在核安全級軟件單元測試上的應(yīng)用研究

★北京廣利核系統(tǒng)工程有限公司 董玲玲，曹宗生，李旗，劉元

Kaputt在核安全級軟件單元測試上的應(yīng)用研究

★北京廣利核系統(tǒng)工程有限公司 董玲玲，曹宗生，李旗，劉元

在核安全級軟件的測試中，單元測試是必不可少的測試手段之一。目前，部分核安全級軟件采用函數(shù)式編程語言O(shè)Caml開發(fā)，但針對該語言開發(fā)的核安全級軟件進(jìn)行單元測試，尚缺乏具體的執(zhí)行標(biāo)準(zhǔn)，通過確認(rèn)測試來補(bǔ)充。本文提出采用第三方測試工具Kaputt對OCaml開發(fā)的核安全軟件進(jìn)行單元測試的方法，介紹Kaputt的測試模式、測試執(zhí)行過程，及測試后分析關(guān)鍵字的覆蓋率，以判斷測試是否完備。該方法已在自主化核安全級軟件測試中進(jìn)行實(shí)踐，取得良好的效果。

函數(shù)式編程；OCaml；Kaputt；單元測試

1 引言

近年來，隨著計算機(jī)軟件在尖端領(lǐng)域的應(yīng)用，如航空領(lǐng)域、軌道交通領(lǐng)域、核電領(lǐng)域，人們與軟件的接觸越來越多，軟件已成為人們生活中的必需品，如果軟件系統(tǒng)的任何一個環(huán)節(jié)工作失敗或遭受攻擊都會帶來難以預(yù)料的后果，給人們的生產(chǎn)和生活帶來巨大的災(zāi)難，甚至造成不可恢復(fù)的創(chuàng)傷，因此軟件安全的重要性與日劇增[1]。

單元測試在軟件開發(fā)過程中起到舉足輕重的作用，它能以較高的效率發(fā)現(xiàn)軟件中潛在的缺陷，在這個階段修改缺陷的成本較低[2]。單元測試是保證軟件質(zhì)量的重要手段。核安全級產(chǎn)品的可靠性一直是核電領(lǐng)域的關(guān)注點(diǎn)，函數(shù)式編程語言O(shè)Caml逐漸應(yīng)用在核安全級軟件的開發(fā)，為防止軟件在使用中出現(xiàn)重大事故，需要對核安全級軟件進(jìn)行完備的測試，因此對OCaml開發(fā)軟件的測試工作的需求顯得尤為迫切。眾所周知，對于C或C++編寫的代碼，可以采用C++TEST或是Testbed工具完成測試，Java編寫的程序可以用Junit作為單元測試工具。對于硬件編程語言Verilog編寫的程序同樣有對應(yīng)的仿真工具Qutasim或Modelsim完成代碼測試。而如何對函數(shù)式語言編寫的程序進(jìn)行單元測試，尚未有公用的測試工具。

目前有針對函數(shù)式編程語言O(shè)Caml編寫的程序測試的工具Kaputt（A Popperian Unit Testing Tool），它能幫助我們進(jìn)行有效的測試，能提供測試相關(guān)的指標(biāo)并顯示，輔助我們完成單元測試工作。

2 函數(shù)式編程語言

目前常用的計算機(jī)語言，如C、Java被稱為命令式編程語言，是以諾伊曼式的計算機(jī)為設(shè)計背景，通過不斷修改存儲帶上的單元值，以一種命令的方式進(jìn)行計算；此外還有一種編程語言為函數(shù)式編程語言，它具有較強(qiáng)的數(shù)據(jù)表達(dá)性，它將計算機(jī)計算視為函數(shù)的計算，由函數(shù)定義和調(diào)用構(gòu)成計算程序，其理論基礎(chǔ)是λ演算，該演算可以接受函數(shù)當(dāng)作輸入（引數(shù)）和輸出（傳出值）[3]。主要的函數(shù)式編程語言有20世紀(jì)80年代末發(fā)布的Haskell語言，它是在Miranda的基礎(chǔ)上得到的，是對Miranda進(jìn)行了標(biāo)準(zhǔn)化，這種語言集合了其他相關(guān)函數(shù)式編程開發(fā)的原理，它無需花費(fèi)太多的贅述就能完成一些數(shù)據(jù)結(jié)構(gòu)，比如鏈表和矩陣。它的語言衍生物有很多，有擴(kuò)充的Haskell、并行Haskell和面向?qū)ο蟮淖凅w如Mondrian等。與此同時，它還被用作為在新語言設(shè)計時的標(biāo)準(zhǔn)模板。另一種函數(shù)式編程語言是Clean，它和Haskell有很多一樣的地方，目前這門語言是用C寫成的，由尼茲梅根大學(xué)負(fù)責(zé)維護(hù)[4]。

此外還有一種函數(shù)式編程語言是OCaml, 近幾年也得到了廣泛的發(fā)展。OCaml最早稱為Objective Caml,是Caml編程語言的主要實(shí)現(xiàn)，開發(fā)工具包含交互式頂層解釋器，字節(jié)編譯器以及最優(yōu)本地代碼編譯器。其中由OCaml編寫的COQ定理證明器在形式化證明領(lǐng)域得到很好的應(yīng)用。OCaml目前由法國國家信息與自動化研究所（INRIA）管理和維護(hù)。

3 Kaputt單元測試方法

INRIA機(jī)構(gòu)提供了OCaml的單元測試工具Kaputt。有兩種測試模式，一種是基于斷言比較的模式，另一種是基于規(guī)范的模式。

斷言比較模式，是指通過斷言比較的方式，簡單判斷函數(shù)的輸出和期望是否相等，從而判斷用例是否執(zhí)行成功。基于說明的模式，是指可以按指定輸入類型隨機(jī)產(chǎn)生用例，并且比較輸入和輸出。這種模式，并不能支持復(fù)雜的類型，僅限于通用的類型，比如int、string這類比較簡單的。本質(zhì)上，基于說明的模式是斷言比較模式的改進(jìn)。

3.1 斷言模式

斷言模式的測試流程如圖1所示。

圖1 斷言模式的測試流程

Kaputt軟件的斷言模式，需要對測試的代碼塊進(jìn)行分析，識別單元測試用例，從用例中抽取斷言，將斷言通過runtest函數(shù)與被測試的代碼關(guān)聯(lián)在一起，運(yùn)行runtest，可得出結(jié)果，通過會提示pass,不通過提示faild，并給出期望值。

OCaml函數(shù)的特點(diǎn)，分支多、參數(shù)層層嵌套、逐層展開，利用“矩陣輸入法”，構(gòu)造輸入，進(jìn)一步判斷函數(shù)的運(yùn)行流程和期望結(jié)果。

以一個tanslate_call_assign為例，該函數(shù)為遞歸函數(shù)，參數(shù)有(lhs_list,lrv,cids,lids)函數(shù)內(nèi)部又調(diào)用了assign_check函數(shù)，還有一些case條件（e,t,t0）。輸入的測試用例，應(yīng)該以lhs_list,lrv,cids,lids,e,t,t0為對象構(gòu)造，用矩陣的每行對應(yīng)這些輸入變量，末尾再加上Output，矩陣的每列則代表每個變量的取值，每一行，對應(yīng)了函數(shù)的一種分支，這樣用矩陣輸入法可以清晰地把用例表示出來，如表1所示：

表1 矩陣輸入法構(gòu)造測試用例

3.2 規(guī)范模式

Kaputt基于規(guī)范的測試是由函數(shù)Test.make_ random_test生成，由9部分構(gòu)成：（1）文件名；（2）整型的數(shù)字，用于規(guī)定生成多少個用例；（3）生成規(guī)范匹配的數(shù)值；（4）分類器，把生成的測試用例進(jìn)行分類；（5）簡化器，用來生成最小的反例；（6）隨機(jī)激勵源；（7）生成器；（8）被測試的函數(shù)；（9）規(guī)范；下面表格的代碼是采用基于規(guī)范的測試設(shè)計，測試生成的字符串是短型的還是長型的。

表2 規(guī)范模式的測試用例設(shè)計

4 Kaputt單元測試應(yīng)用

Kaputt斷言的測試方法與常見的測試方法相似，當(dāng)輸入測試用例時，要預(yù)測出相應(yīng)的測試結(jié)果，用斷言assert將期望值與實(shí)際值進(jìn)行比較，當(dāng)數(shù)值不一致時報測試失敗。在測試代碼前，需要打開Kaputt. Abbreviations；通過Test.make_assert_test函數(shù)聲明使用的斷言的方式測試，具體步驟為：（1）聲明文件名；（2）建立一個函數(shù)；（3）assert斷言聲明預(yù)期值；（4）測試用例執(zhí)行。

對冪函數(shù)進(jìn)行測試：

用遞歸的方法定義一個冪函數(shù)：

(fun() -〉A(chǔ)ssert.equal_float 81537.26976 power(5 9.6))

Let () = Test.run_tests[t1,t2,t3];

測試后，顯示的結(jié)果如下：

val power : int -〉 float -〉 float = 〈fun〉

val t1 : Kaputt.Test.t = 〈abstr〉

val t2 : Kaputt.Test.t = 〈abstr〉

val t3 : Kaputt.Test.t = 〈abstr〉

Test 'test case 1' ... passed

Test 'test case 2' ... passed

Test 'test case 3' ... passed

所有的測試用例均通過。

5 工程實(shí)踐應(yīng)用

編譯器是圖形化核安全級軟件集成開發(fā)環(huán)境中的一個重要工具，它能把圖形模型或者文本模型轉(zhuǎn)換成等價的C程序。目前，為保證翻譯的可信性，有些工具的開發(fā)內(nèi)部嵌入形式化驗(yàn)證的方法，比如實(shí)時嵌入式系統(tǒng)SCADE，它通過直觀的圖形化的建模和模擬仿真，再經(jīng)過形式化驗(yàn)證，自動生成可直接面向工程的標(biāo)準(zhǔn)C代碼[5～8]，保證了軟件需求和代碼執(zhí)行的高度同步。

為實(shí)現(xiàn)數(shù)字化核儀控設(shè)備的自主化，我們開發(fā)了一套類似功能的可信翻譯器，將圖形化的語言Lustre與形式化驗(yàn)證工具Coq結(jié)合，完成C代碼的翻譯工作。其中部分形式開發(fā)工作采用OCaml實(shí)現(xiàn)，為驗(yàn)證該部分程序的正確性，可應(yīng)用OCaml單元測試工具Kaputt完成，如圖2所示。

圖2 可信編譯器開發(fā)過程

采用Flex和Bison工具對被翻譯的Lustre語言進(jìn)行詞法、語法的分析，抽象出其中的語法樹，對該語法樹進(jìn)行靜態(tài)語義檢查，然后在COQ平臺上開發(fā)相應(yīng)的程序，將Lustre＊AST轉(zhuǎn)換Lustre-AST，最終把Lustre-AST翻譯成可下裝的C語言，完成從Lustre語言到C的翻譯過程。最后一步采用了OCaml語言開發(fā)，同時采用基于COQ定理證明的方式保證該步的正確性。針對OCaml開發(fā)的部分可采用單元測試的方式提高安全性。

5.1 測試環(huán)境搭建

首先將所有被測的后綴為.ml函數(shù)編譯成一個庫文件，庫文件的后綴為.cma格式。可針對每個文件或每個函數(shù)編寫一個測試文件，編譯時鏈接上庫文件和Kaputt、Bisect的庫文件，就能得到可執(zhí)行的測試程序。這種環(huán)境有效保證了每個測試人員的工作獨(dú)立性，并且容易統(tǒng)計測試結(jié)果。

測試的輸入直接為測試用例的文件，比如設(shè)定.ast為測試用例的文件，觀察覆蓋率。如輸入語句：run:

BISECT_FILE=coverage ./bytecode srs_ l2c_syn_001.ast

5.2 測試結(jié)果

測試結(jié)果如表3、表4所示，關(guān)鍵語句if/then、for、whlie均有覆蓋率顯示。驅(qū)動模塊Driver.ml覆蓋率為82%，打印語義分析模塊printCsyntax.ml覆蓋率為43%等。通過Kaputt軟件的測試，可以統(tǒng)計出關(guān)鍵字的覆蓋率，對未覆蓋到的部分，測試人員可進(jìn)行分析，是由于測試用例不夠全面未覆蓋到，還是防御性編程的原因沒有覆蓋到，并給出分析結(jié)果，此外該軟件還顯示出每個文件的關(guān)鍵字覆蓋率，達(dá)到單元測試的目的。

If/then 434/794(54%) Class value 0/0(-%) try 4/4(100%) Top level expression 18/18(100%) while 0/0(-%) Lazy operator 97/198(48%) Match/function 876/2004(43%)

表4 每個文件覆蓋率

6 結(jié)語

單元測試在軟件開發(fā)的生命周期中是不可或缺的一步，它能以最低的成本保證軟件的可靠性。本文介紹的基于Kaputt的OCaml單元測試方法的研究解決了工作中遇到OCaml編寫的程序無法進(jìn)行單元測試的難題，該方法在工程實(shí)踐中得到了進(jìn)一步的應(yīng)用，可以觀察軟件中的關(guān)鍵字的代碼覆蓋率是否滿足要求，提高代碼測試的效率。

[1] 譙婷婷, 王樂, 王芳, 等. 基于Coq的軟件安全性驗(yàn)證研究與實(shí)現(xiàn)[J]. 計算機(jī)工程與應(yīng)用, 2012, ( A02 ) : 96 - 100.

[2] 郭榮. 基于Testbed的C++單元測試（動態(tài)測試）方法[J]. 網(wǎng)絡(luò)安全技術(shù)與安全, 2014 （3）: 56 - 59.

[3] 陳付龍. 函數(shù)式程序設(shè)計語言的教學(xué)研究與探討[J]. 福建電腦, 2010, ( 6 ) : 23.

[4] 王學(xué)瑞. 函數(shù)式編程語言發(fā)展及應(yīng)用[J]. 計算機(jī)光盤軟件與應(yīng)用，2012（ 23 ）: 181 - 182.

[5] 林楓. 基于SCADE的形式化驗(yàn)證技術(shù)研究[J]. 測控技術(shù), 2011, 30（ 12 ）:71 - 74.

[6] 陳鋼, 宋曉宇, 顧明. COQ定理證明器輔助PLC程序驗(yàn)證和分析[J]. 北京大學(xué)學(xué)報(自然科學(xué)版)，2010, 46（1） ：30 - 34.

[7] 董威. 單元測試及測試工具的研究與應(yīng)用[J]. 微型電腦應(yīng)用，2008, 24（5） ：24 - 26.

[8] 顏雯清, 李秀娟. SCADE平臺下C代碼的自動生成[J]. 計算機(jī)仿真，2007, 24（10）：264 - 268.

Research of Kaputt Application in the Unit Testing of Nuclear Safety Grade Software

In nuclear software testing, the unit testing is one of the essential testing methods. At present, a part of nuclear safety grade software adopted the functional programming language OCaml for development, but the unit test of nuclear safety grade software developed by OCaml lacks specific execution standard, and supplement by validation tests. This article presents a method of unit testing for nuclear safety software developed by OCaml using third party test tool Kaputt, and introduces the testing mode, test execution process and the coverage of keyword after testing to judge whether the test is complete. This method was applied in autonomous nuclear safety software testing, obtaining good results.

Functional programming；OCaml; Kaputt; Unit testing

董玲玲（1986-），女，山東德州人，助理工程師，碩士，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要從事單元測試、可編程邏輯驗(yàn)證工作。

曹宗生（1976-），男，遼寧沈陽人，高級工程師，學(xué)士，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要從事核電站數(shù)字儀控系統(tǒng)產(chǎn)品質(zhì)量控制及測試工作。

李 旗（1977-），男，黑龍江哈爾濱人，工程師，現(xiàn)就職于北京廣利核系統(tǒng)工程有限公司，主要從事系統(tǒng)測試工作。

劉 元（1973-），女，遼寧凌海人，高級工程師，碩士，現(xiàn)任北京廣利核系統(tǒng)工程有限公司公司副總工，主要從事核電項目的技術(shù)決策工作。