1
关注中国自动化产业发展的先行者!
2024
2024中国自动化产业年会
2023年工业安全大会
OICT公益讲堂
当前位置:首页 >> 案例 >> 案例首页

案例频道

嵌入式操作系统数学库函数测试方法研究和应用
核鹭操作系统数学库以C语言函数库的形式提供常用的若干数学函数,被用于核安全重要的仪控系统,直接参与核安全重要功能的实现,因此必须在使用前对其进行全面验证和确认。为提高测试全面性、有效性和测试执行的自动化程度,研究者采用对比测试方法完成测试工作,以保证各函数的计算正确性和精度:首先在参考环境(通用PC机)下,按照IEC 60559中浮点数定义和各待测函数定义域和计算方法等特性,生成各待测函数输入值序列并在参考环境下调用编译工具内置的库函数计算出对应的函数输出值,再将已产生的各待测函数输入值序列和对应的函数输出值以二进制文件方式保存并传递给嵌入式操作系统目标机运行环境,并在目标机运行环境下调用嵌入式操作系统数学库函数计算各待测函数输入值序列的对应函数输出值,最后以二进制值的方式比较不同环境下的函数输出值,分析测试中发现的问题以及计算误差产生原因和可接受条件,最终确保嵌入式操作系统数学库函数在其定义域内计算正确并在可接受的误差范围内。

★北京广利核系统工程有限公司程建明,徐先柱

关键词:嵌入式操作系统;数学库函数;对比测试;误差分析

核鹭操作系统(NuEgretOS)是北京广利核系统工程有限公司开发的嵌入式多任务操作系统软件,可运行于基于龙芯2K1000处理器的专用硬件环境中,为执行核安全重要功能的、符合包含IEC 62138-2018[1]等标准要求的应用软件提供操作系统软件环境。NuEgretOS提供在目标硬件环境下资源分配、调度、输入输出控制以及数据管理等服务,应用软件在此基础上提供信号和控制处理逻辑。NuEgretOS还提供部分C语言标准库函数(其中包含数学库函数),供基于NuEgretOS运行的应用软件设计时调用。其中,NuEgretOS数学库目前提供最常用的若干数学函数,包括三角函数、反三角函数、双曲函数、指数和对数函数、幂函数,以及与浮点数特性相关的函数(如取整、取余、取绝对值、切分浮点数)等。

出于安全方面的原因,NuEgretOS数学库实现过程中不使用任何第三方函数库,包括不调用编译器自带的数学函数库中的函数。同时,由于NuEgretOS数学库函数将直接参与应用软件处理逻辑,执行包括核安全重要功能在内的应用软件功能,因此在使用前必须对其进行全面验证和确认。通过测试保证其正确性和计算精度是NuEgretOS数学库验证和确认的重要工作之一。

1 库函数设计NuEgretOS软件和应用软件均使用C语言及必要的

汇编语言开发,使用GCC工具进行编译。NuEgretOS以镜像文件(.bin文件)方式存储于目标硬件中的存储器上,并在设备上电时加载运行。NuEgretOS的C语言标准库(其中包含数学库函数)以库文件(.a文件)的形式提供给应用开发环境,并与应用软件代码一起编译生成可执行与可链接格式文件(elf格式,.out文件),由NuEgretOS加载和运行。

NuEgretOS数学库(C语言标准库的一部分)中的全部函数定义和POSIX.1-2017[2]标准中对应的函数相同,是POSIX.1-2017规定的数学函数的子集。

NuEgretOS数学库各函数输入和输出中的数学上定义为实数的数值均使用double类型浮点数表示,该浮点数类型符合ISO/IEC 60559:2020(IEEE Std754-2019)[3]对64位双精度浮点数(binary64)的规定。double型数据位串定义如图1所示。

image.png

图1 double型数据位串定义

按该标准定义,double型数以64位位串值(二进制内存值)表示实数域内的若干个(264-253-1,约1.84×1019个)离散数值(有限小数,含整数)以及计算机在处理小数运算时的特殊定义值(不表示任何实数的位串值,仅用于计算机对浮点数处理的特殊情况的表示)。double型数据位串值定义细分类别及特点如表1所示。

表1 double型数据位串值定义细分类别及特点

image.png

2 测试设计

2.1 计算误差来源分析

基于ISO/IEC60559:2020(IEEE Std754-2019)[3]对64位双精度浮点数(binary64)的规定,双精度浮点数除特殊定义值外,两个位串值相邻的浮点数数值之间的差值的绝对值定义为1个ULP(unit in the last place,最小有效数)。1ULP的实际表示值与指数域的大小相关:当指数域为最大值0x7FE时,1ULP≈8.99E307;当指数域为最小值0x000时,1ULP≈4.94E-324。对于浮点数表示范围(约-1.79E308~约1.79E308)内的任意实数,在最近舍入模式下,由浮点数离散特性带来的最大表示误差≤0.5ULPs。规格化数的二进制有效数字个数为53个,由浮点数舍入带来的最大表示误差(≤0.5ULPs)带来的数值相对误差范围为(2-54,2-53),非规格化数的二进制有效数字个数最大为52个,随数值减小而减少,由浮点数舍入带来的最大表示误差(≤0.5ULPs)造成的数值相对误差也相应增大,范围为(2-53,2-1)。

对于NuEgretOS数学库中与浮点数特性相关的算术函数(如取整、取余、取绝对值、切分浮点数等),函数的运算输出与其理论输出之间不应存在误差,即允许误差为0ULPs。而对于其它函数,包括三角函数、反三角函数、双曲函数、指数和对数函数、幂函数等,其理论计算值与其函数输出值之间的误差受多种因素影响,主要包括:

(1)输入值表示误差;

(2)计算方法误差,如使用泰勒展开式有限项带来的误差;

(3)计算过程误差,包括模型参数引入的误差、中间计算结果的舍入误差等;

(4)输出值表示误差。基于NuEgretOS数学库函数的目标应用,除算术计算函数外,设定各函数输出的允许误差为2ULPs。

2.2 验证目标

基于NuEgretOS数学库的设计特点和应用要求,NuEgretOS数学库的验证目标包括:

(1)各函数在其定义域内的任意值(包括浮点定义的正负零值)的计算输出值正确(符合函数定义)且在允许误差范围内。

(2)各函数对异常及特殊情况处理正确,包括对计算值超浮点表示范围的处理、输入非函数定义域数值、输入浮点特殊定义值等,函数输出符合处理器特性以及IEC60559规定的特殊定义值。如有定义,NuEgretOS应用软件可通过注册中断处理程序获知计算过程例外或异常并处理。

2.3 测试方案

NuEgretOS数学库为新开发软件,各函数遵循其数学定义,其输出值实数范围内存在理论精确值,该理论精确值在确定的浮点数类型定义和舍入方式下,经计算机计算后输出的浮点数(二进制内存值)是唯一的和确定的,与函数的实现方式以及运行所依赖的硬件和软件环境无关。同时,NuEgretOS数学库范围内的各函数已在支持POSIX标准的大多数软件开发工具及编译工具中实现。这些已实现的函数多包含在随软件开发工具及编译工具提供的函数库中,其实现比较成熟且已有较多运行经历,运算结果相对可信,NuEgretOS数学库测试时假定对应函数的预期运算结果。当运算结果一致时,可在较高可信度上证明NuEgretOS数学库函数的正确性和精度,当运算结果不一致时,进行函数实现分析以定位问题或通过设计分析证明NuEgretOS数学库函数的正确性和精度。测试前对NuEgretOS数学库全部函数的设计和实现代码的评审和分析也是保证NuEgretOS数学库函数的正确性和精度的措施。因此,可以通过对比其它已实现的成熟函数库执行结果的方式,对NuEgretOS数学库的正确性和精度进行对比测试。NuEgretOS数学库对比测试总体方案如图2所示。

image.png

图2 对比测试方案

分别建立数学库的参考运行环境和目标机运行环境,目标机运行环境和NuEgretOS应用软件运行环境完全一致。在参考运行环境下,可以用与NuEgretOS应用程序相同的方式调用相同定义的各数学库函数。参考运行环境由通用PC机搭建,同时作为测试应用程序的开发环境。

用相同的方式分别建立参考环境测试工程和目标机测试工程,两个测试工程共用一套C语言代码,两个工程中的测试应用程序内必要的有差别的行为通过预编译开关实现。测试应用程序中含用例生成、用例执行、结果保存、用例读取、结果比较等主要功能模块。参考环境应用程序实际执行用例生成、用例执行、结果保存三项功能。参考环境测试应用程序运行结果保存中包括了测试用例中各函数的输入序列和其在参考环境中的运算结果。各函数的输入序列和对应的参考环境运算结果组成测试向量,以二进制内存拷贝的方式保存成文件,并下载到目标机运行环境。目标机测试应用程序读取各待测函数测试向量生成测试用例。目标机测试应用程序执行完成测试用例后进行结果比较,以文件和串口打印输出的形式输出与参考环境计算结果的比较情况。同时目标机测试应用程序用与参考环境测试应用程序相同的方式保存测试结果。参考环境和目标机处理器大小端模式相同,测试向量的保存、传递和读取过程不引入浮点数表示误差。参考环境和目标机的测试应用程序的全部输出作为人工分析的输入,用以最终判定NuEgretOS数学库的正确性和计算精度是否符合设计和应用目标。

另外,还使用不同的编译工具生成多个参考环境测试应用程序并对其运算结果进行比较,用以提高参考环境测试应用程序运算结果作为NuEgretOS数学库预期结果的可信度。

2.4 测试用例生成

在本项测试中,各函数的测试输入覆盖率是保证对NuEgretOS数学库各函数测试全面性的最重要指标。由于double型数据位串值个数(264)远大于目标机运行环境可执行测试输入数量,进行位串值完全穷举是不可行的,需按适当的规则进行抽样。

为保证充分的输入覆盖率,测试用例设计前先分析各函数的基本特性,包括定义域、周期(如有)、单调性、与函数计算机实现方法相关的特殊值等,再根据各函数特性和浮点数定义自动生成测试输入序列。在参考环境测试应用程序中生成各函数测试输入值序列时,需满足以下规则:

2.4.1 插入函数整体定义域边界值、典型周期定义域边界值、函数拐点值,无论函数在这些值上是否有定义;

2.4.2 插入函数整体定义域、典型周期定义域内若干(40个以上)随机值;

2.4.3 插入与各函数实现相关的特殊值,可能包括:

(1)与函数计算方法相关的函数定义域边界值,如sin函数中泰勒展开式计算前x的边界值π/4;

(2)与函数计算所用参数相关的特殊值等;

(3)函数计算过程中可能出现溢出例外的函数定义域值。

2.4.4 插入与浮点数定义相关的特殊值(无论数学函数在这些值上是否有定义),包括正负零、正负无穷大、qNaN(静默非数)/sNaN(信号非数)典型值、规格化数和非规格化数的最大值和最小值。

除自动生成的随机数值外,以上各项中的输入值均以C语言共用体方式直接对内存赋值,以避免因常量编译等因素造成实际输入值与需输入值不一致。另外,在按以上规则插入各函数测试输入值时,同时插入每个输入值的二进制位串值的相邻值。

3 测试工程的编译和运行

在参考环境中,使用MinGW提供的GCC编译工具编译测试工程,编译过程中数学函数调用GCC编译工具自带函数库(libgcc.a)中的对应函数实现,编译后的测试应用程序在Windows操作系统下运行。

目标机测试工程在Windows操作系统下调用GCC编译工具进行交叉编译,编译过程中数学函数调用NuEgretOS数学库(libEgretLibc.a)中的对应函数实现。另外,在参考环境中还调用了MSVC编译器编译测试工程,编译过程中数学函数调用MSVC编译工具自带的C运行时库中的对应函数实现。

4 运行结果比较

4.1 参考环境下不同编译的测试应用程序运算结果比较

Windows操作系统下使用MinGW和MSVC编译的测试应用程序可以相互传递各自生成的二进制测试向量文件。在相同的函数输入下,两个程序的函数运行结果仅存在细微差别,包括:

(1)部分函数在特殊输入值下计算值仅相差1ULP(如sqrt函数输入最大规格化数,sin/cos函数的部分输入值)。

(2)部分函数在输入为NaN时,输出的NaN位串值不同(如fabs函数是否将NaN位串值的符号位设置为0,exp函数输出NaN时是否将位串值尾数域的全部非首位设置为0),对NaN的不同处理均不违反C99[4]和POSIX.1-2017标准的要求。

结合MinGW和MSVC编译工具(包括工具自带的函数库)的应用广泛程度和函数输出比较结果,以MinGW编译工具生成的参考环境测试应用程序的运算结果作为NuEgretOS数学库各函数的参考值是相对可信的。

4.2 参考环境和目标机运行环境测试应用程序运算结果比较

以MinGW作为参考环境测试应用程序编译工具,并以该参考环境测试应用程序生成的各函数输入序列作为目标机测试应用程序的被测函数输入序列,假定该参考环境测试应用程序对自身生成的测试输入序列的函数运算结果为目标机测试应用程序执行NuEgretOS数学库各函数的预期结果(即参考值)。经目标机测试应用程序运行结果比较,除以下两项主要问题外,NuEgretOS数学库运算结果符合验证目标:函数对有定义输入值、异常及特殊情况处理正确,并且函数输出为有限小数值的计算误差≤2ULPs。

(1)问题1:exp、sinh、sqrt、log、log10这5个函数输入为非规格化浮点数时,计算值错误。部分测试结果如表2所示。

表2 问题1测试结果

image.png

(2)问题2:cos、sin、tan这三个周期性函数在输入值较大时,计算误差超允许值(2ULPs)。部分测试结果如表3所示。

表3 问题2测试结果

image.png

5 问题分析和处理

经过对已发现的两个问题(如表2和表3所示)相关的软件代码进行分析和调试,两个问题的原因和处理方式如下:

(1)问题1,属例外处理的汇编代码错误。错误原因为汇编代码中寄存器使用错误,使得NuEgretOS在处理龙芯2K1000浮点协处理器(FPU)的例外(未实现操作例外,2K1000未实现的MIPS64全部浮点指令)时的处理逻辑出现错误。汇编代码修改后问题得到解决。经回归测试,这5个函数(exp、sinh、sqrt、log、log10)在参考环境和目标环境的计算误差不超过2UPLs,符合NuEgretOS数学库预先设定的要求。

(2)问题2,由计算参数表示误差而引起的中间计算值误差随三角函数2π周期数扩大。NuEgretOS数学库在实现cos、sin、tan这三个周期性函数,其中sin和cos函数采用这两个函数的泰勒展开式求解,tan函数利用tanx=sinx/cosx关系式求解。在代入泰勒展开式前,将输入值x通过三角函数变换公式整理到绝对值不大于π/4的弧度值。首先需利用公式(如sinx=sin(k·2π+θ),x∈R,k∈N,θ∈[-π,π])将NuEgretOS数学库中的三角函数定义域转化到±π之间时,使用位串值为0x401921FB54442D18的参数(名为PI2)表示理论数值2π,其表示值(6.283185307179586231996)与精确值(6.283185307179586476925)之间的表示误差为δPI2≈2.449×10-16,约0.276ULPs。经过k个2π周期后,造成θ值的误差为δθ=k·δPI2,因此|k|≥1时,这一单一因素将可以造成函数值误差大于2ULPs。解决这一问题可以有两个途径:

(1)限制函数输入值的范围,以减少中间值θ的计算误差;

(2)使用更高精度的浮点数(如binary128或两个binary64)表示2π的值并参与计算。

6 总结

研究者引入对比测试方法快速准确地实现了对新开发的嵌入式操作系统数学库的测试,并通过误差分析辅助完成了对测试中发现的被测函数问题的定位和处理,提高了被测试函数库的计算精度和结果可信度。

按照经分析确定的规则生成各被测试函数输入值序列保证了测试的有效覆盖率。

在参考环境中采用不同编译工具并调用不同工具自带函数库执行相同输入序列的函数计算,并对计算结果进行比较,提高了参考环境生成的、拟作为目标机环境被测函数预期值的函数值的正确性和精度的可信度。

使用浮点数内存值二进制方式保存、传递和比较各函数的输入序列和对应的参考环境运算结果组成的测试向量,避免了浮点数值在不同环境中交换和比较可能带来的表示误差和比较不确定性。

通过参考环境和目标环境测试应用程序,测试用例按规则自动生成、执行并比较结果,提高了本项测试的自动化程度。

作者简介:

程建明(1976-),男,四川人,高级工程师,学士,现就职于北京广利核系统工程有限公司,主要从事核安全级软件的验证和确认工作。

徐先柱(1982-),男,黑龙江人,高级工程师,学士,现就职于北京广利核系统工程有限公司,主要从事于核安全级软件的验证与确认工作。

参考文献:

[1] IEC 62138-2018, Nuclear power plants-Instrumentation and control systems important to safety-Software aspects for computer-based systems performing category B or C functions[S]. International Electrotechnical Commission,2018.

[2] POSIX.1-2017/IEEE Std 1003.1-2017,IEEE Standard for Information Technology-Portable Operating System Interface (POSIX®) [S]. IEEE Computer Society and The Open Group, 2017.

[3] ISO/IEC 60559:2020(E) IEEE Std 754-2019, Floating-point arithmetic[S]. 2020.

[4] ISO/IEC 9899:1999 Programming languages-C[S]. 1999.

摘自《自动化博览》2023年11月刊

热点新闻

推荐产品

x
  • 在线反馈
1.我有以下需求:



2.详细的需求:
姓名:
单位:
电话:
邮件: