国产欧美日韩精品a在线观看-国产欧美日韩精品一区二区三区-国产欧美日韩精品综合-国产欧美中文字幕-一区二区三区精品国产-一区二区三区精品国产欧美

★北京廣利核系統工程有限公司程建明，徐先柱

關鍵詞：嵌入式操作系統；數學庫函數；對比測試；誤差分析

核鷺操作系統（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所示。

圖1 double型數據位串定義

按該標準定義，double型數以64位位串值（二進制內存值）表示實數域內的若干個（264-253-1，約1.84×1019個）離散數值（有限小數，含整數）以及計算機在處理小數運算時的特殊定義值（不表示任何實數的位串值，僅用于計算機對浮點數處理的特殊情況的表示）。double型數據位串值定義細分類別及特點如表1所示。

表1 double型數據位串值定義細分類別及特點

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所示。

圖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測試結果

（2）問題2：cos、sin、tan這三個周期性函數在輸入值較大時，計算誤差超允許值（2ULPs）。部分測試結果如表3所示。

表3 問題2測試結果

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月刊