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-），女，辽宁凌海人，高级工程师，硕士，现任北京广利核系统工程有限公司公司副总工，主要从事核电项目的技术决策工作。