Kaputt在核安全級軟件單元測試上的應用研究

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

Kaputt在核安全級軟件單元測試上的應用研究

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

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

函數式編程；OCaml；Kaputt；單元測試

1 引言

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

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

目前有針對函數式編程語言OCaml編寫的程序測試的工具Kaputt（A Popperian Unit Testing Tool），它能幫助我們進行有效的測試，能提供測試相關的指標并顯示，輔助我們完成單元測試工作。

2 函數式編程語言

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

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

3 Kaputt單元測試方法

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

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

3.1 斷言模式

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

圖1 斷言模式的測試流程

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

OCaml函數的特點，分支多、參數層層嵌套、逐層展開，利用“矩陣輸入法”，構造輸入，進一步判斷函數的運行流程和期望結果。

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

表1 矩陣輸入法構造測試用例

3.2 規范模式

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

表2 規范模式的測試用例設計

4 Kaputt單元測試應用

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

對冪函數進行測試：

用遞歸的方法定義一個冪函數：

(fun() -〉Assert.equal_float 81537.26976 power(5 9.6))

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

測試后，顯示的結果如下：

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 工程實踐應用

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

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

圖2 可信編譯器開發過程

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

5.1 測試環境搭建

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

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

BISECT_FILE=coverage ./bytecode srs_ l2c_syn_001.ast

5.2 測試結果

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

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 結語

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

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

[2] 郭榮. 基于Testbed的C++單元測試（動態測試）方法[J]. 網絡安全技術與安全, 2014 （3）: 56 - 59.

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

[4] 王學瑞. 函數式編程語言發展及應用[J]. 計算機光盤軟件與應用，2012（ 23 ）: 181 - 182.

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

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

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

[8] 顏雯清, 李秀娟. SCADE平臺下C代碼的自動生成[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-），女，山東德州人，助理工程師，碩士，現就職于北京廣利核系統工程有限公司，主要從事單元測試、可編程邏輯驗證工作。

曹宗生（1976-），男，遼寧沈陽人，高級工程師，學士，現就職于北京廣利核系統工程有限公司，主要從事核電站數字儀控系統產品質量控制及測試工作。

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

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