RTOS測驗（韓國方案）

簡介

在本文中，我們重點討論了實時作業系統的驗證和測驗程式，

測驗的目的有兩個，一個是顯示經過驗證的模型屬性是否被繼承到了代碼中，另一個目的是發現代碼的錯誤要檢查結構覆寫率和功能等，

在測驗所開發的作業系統軟體后，我們將其與數字工廠保護系統（DPPS Digital Plant Protection System）軟體一起嵌入測驗板中，該軟體模擬安全關鍵的反應堆保護功能，開發的系統應該滿足10的-3方的故障概率（pfd failure on demand），以表明它對安全關鍵應用是足夠可靠的，我們通過在測驗板上進行必要數量的測驗來證明這一點，

方法

方法分為三部分：

• 在生命周期的每個階段進行規范和驗證
• 為軟體測驗生成測驗資料
• 進行嵌入式系統測驗

2.1 軟體規范和驗證

我們用圖形化的形式化語言來規范實時作業系統，并用模型檢查來驗證它，我們使用STATEMATEMAGNUM工具集，I-Logix，作為形式語言和模型檢查器，STATEMATE MAGNUM是基于活動圖和狀態圖的，
活動圖用于功能描述，狀態圖用于系統的行為描述，狀態圖是一種具有數學語意的定義明確的形式語言，使用狀態圖，我們可以用狀態和它們之間的轉換來描述需求/設計階段的行為，狀態圖中的過渡是五元組（源，目標，事件，行動，條件），狀態圖中的箭頭從源頭到目標，被標記為e[c]/a，這意味著當條件c為真時，事件e觸發了過渡，當過渡時，行動 "a "被執行，行動'a'可以是一個行動的串列，

STATEMATE有一個仿真工具來驗證系統設計，利用仿真，我們不僅可以驗證每個模塊，還可以驗證整個系統，

STATEMATE MAGNUM還提供ModelChecker作為形式驗證工具，
模型檢查可用于檢查設計中關于特定屬性的動態行為，重要的是要知道，模型檢查與傳統意義上的測驗不同，與測驗相反，模型檢查在數學意義上是完整的，如果模型檢查器證明了一個特定的屬性在模型中得到了滿足，那么結果就是100%正確的，如果模型檢查器顯示STATEMATE設計中的一個基本狀態是不可達到的，這意味著沒有人會找到仿真運行（只有輸入變數在執行程序中可以改變），其中的跟蹤路徑包括特定的基本狀態，因此，模型檢查可以被稱為窮舉測驗，所有這些設計資訊都由工具自動翻譯成模型檢查器內核的輸入語言，另一方面，用戶必須定義要檢查的屬性，

我們可以從STATEMATE的代碼生成器中得到一個自動生成的代碼，預計它的錯誤會比人工實作的少，

2.2 軟體測驗

實時作業系統的測驗以兩種方式進行：在軟體測驗和嵌入式系統測驗，軟體測驗的重點是RTOS軟體本身，而嵌入式系統測驗的重點是與嵌入RTOS的應用軟體的集成，

在單元測驗的情況下，我們通過對代碼應用白盒測驗標準來選擇單元測驗資料，這些代碼是在實作階段從STATEMATEMAGNUM自動生成的，我們還通過對設計階段指定的Statecharts應用分支覆寫標準來選擇單元測驗資料，在集成測驗的情況下，我們通過利用設計階段指定的Statecharts來選擇集成測驗資料，在系統測驗的情況下，我們通過利用需求階段指定的活動圖來選擇系統測驗資料，

2.3 嵌入式系統測驗

作為這個測驗的標準，我們設定了千分之一的故障要求，這被用作安全關鍵型核系統的可靠性測驗標準，作為測驗資料，我們生成隨機的故障條件組合，直到它滿足獲得所需的故障數量，

參考資料

• 軟體測驗精品書籍檔案下載持續更新 https://github.com/china-testing/python-testing-examples 請點贊，謝謝！
• 本文涉及的python測驗開發庫 謝謝點贊！ https://github.com/china-testing/python_cn_resouce
• python精品書籍下載 https://github.com/china-testing/python_cn_resouce/blob/main/python_good_books.md

形式化規范和驗證程式

3.1 實時作業系統的要求

實時作業系統與一般的作業系統不同，它的邏輯正確性不僅取決于其輸出的正確性，而且還取決于其輸出的及時性，此外，像其他作業系統一樣，必須至少提供以下三種功能：任務調度、任務分發和任務間通信，調度是決定下一個控制CPU的任務的程序，當中斷發生時，它被呼叫，任務完成其作業，正在運行的任務被暫停，

當調度器被呼叫時，它掃描準備就緒狀態的任務串列，根據調度策略選擇任務，并將CPU控制權交給它，調度是一個切換、保存和恢復運行任務和下一個運行任務的背景關系的程序，在本文中，調度員定期創建任務并使其處于準備狀態，任務內通信使任務能夠交換資訊并相互同步，訊息郵箱和訊息佇列被實作來執行任務間的通信，

用戶代碼作為一個任務被執行，有預定的執行時間和周期，作業系統可以在任何用戶任務的執行程序中打斷它，

3.2 實時作業系統規范和驗證

實時作業系統的功能規范如圖3.1所示，每個方框都包括實時作業系統的功能，線代表功能之間的通信，虛線框代表外部環境，實時作業系統包含內核、中斷處理程式和任務，內核包括調度器、任務管理器、訊息信箱和訊息佇列，任務模塊有七個任務：五個任務的優先級相同，一個任務的優先級更高，最后一個被分配為空閑任務，

調度器的行為規范調度器執行基于優先級的，或者說是輪回的調度，RTOS中的嵌入式軟體在其應用中有兩個不同的任務，一個是監控和投票任務，另一個是行程任務，跳閘（關機）任務有最高的優先級，其他任務有相同的優先級，
圖3.2顯示了調度器模塊內部的行為，
對于任務間的通信，我們的實時作業系統提供了訊息郵箱和訊息佇列，

圖3.3顯示了任務的行為，每個任務基本上有五個狀態：休眠、準備、運行、等待和ISR，休眠狀態表示任務未被創建，處于休眠狀態的任務可以在任務進入它的時期并花費抵消時間后被創建，處于準備狀態的任務正在等待調度，而調度已經準備好運行，處于運行狀態的任務在需要使用資源或花費時間時過渡到等待狀態，當運行中的任務被系統打斷時，將過渡到ISR狀態，調度器模塊被用來喚醒任務，
在規范之后，使用STATEMATE對RTOS進行仿真，如圖3.4所示，

圖3.4 RTOS的模擬通過ModelChecker驗證的屬性如下：

• 指定的RTOS是否有不可到達的狀態，
• 指定的實時作業系統是否是確定性的，
• 兩個或多個任務是否可以同時處于運行狀態，

其結果如圖3.5所示，

在Statecharts中的設計規范可以自動翻譯成C代碼，在后面的階段進行測驗，

4. 軟體測驗

4.1 單元測驗

在RTOS的單元測驗中，單元從Statecharts中提取出來，并分別自動轉換為C代碼，單元測驗有兩個目的：一個是識別自動轉換的C代碼是否正確，另一個是檢查代碼的行為是否與我們設計的一致，

4.2 基于狀態的單元測驗

我們通過應用分支覆寫標準，從Statecharts中指定的單元中提取基于狀態的單元測驗資料，分支覆寫標準需要覆寫所有的轉換，之所以選擇這個標準，是因為規范本身是基于狀態和它們之間的轉換，
為基于狀態的單元測驗生成測驗資料的程式如下，

• (1) 識別要測驗的單元，
• (2) 為基于狀態的單元測驗選擇測驗資料，
  • 對從設計規范中提取的單元應用分支覆寫標準，
  • 選擇測驗資料來覆寫所有的分支以滿足標準，

我們使用結構測驗工具ATAC（Automatic Test Analysis for C進行基于代碼的測驗，我們選擇兩個白盒測驗標準：陳述句覆寫標準和分支覆寫標準，陳述句覆寫率標準是按照Reg.Guide 1.171中對核應用的建議選擇的，根據Reg.Guide 1.171，我們應該在基于代碼的測驗中覆寫代碼中的所有陳述句，
在這個測驗中，分支覆寫標準也被選為一個更有力的標準，
為基于代碼的單元測驗生成測驗資料的程式如下，

• (1) 識別要測驗的單元，
• (2) 為確定的單元逐一生成自動代碼，
• (3) 為基于代碼的單元測驗選擇測驗資料，
  • 對代碼應用陳述句和分支覆寫標準，
  • 選擇資料

4.2 集成測驗

集成測驗的目的是檢查當單元結合在一起時是否有任何錯誤，因此，它側重于模塊之間的介面，我們選擇能夠檢測模塊間介面資訊的測驗資料，選擇集成測驗資料的程序如下所示：
(1) 繪制狀態組合圖，

• 確定要組合成一個模塊的單元，這在圖4.2中顯示，模塊和單元分別用圓角矩形和橢圓表示，初始單元用一個帶復選標記的橢圓表示，一個最終單元用兩個橢圓表示，
• 單位之間的關系用虛線表示，模塊之間的關系用實線表示，

(2) 在狀態組合圖中，一個狀態代表單元或模塊，而一個過渡則代表狀態之間的通信關系，通過應用分支覆寫標準，我們可以覆寫狀態組合圖中的所有狀態和分支，因此，通過應用分支覆寫標準選擇的測驗資料覆寫了狀態分解圖中的所有符號，

4.2.1 實時作業系統的狀態組合圖

(1) 確定組合成模塊的單元 圖4.3是實時作業系統的狀態組合圖，有兩個模塊：
內核和任務模塊，這些模塊分別由兩個和八個單元組成，
(2) 識別關系 如圖4.3所示，如果任務模塊得到SYS_ON信號，任務模塊中的 "任務 "單元會向內核模塊發送TCB_RDY信號，然后，內核模塊發送RUN_TSK信號來啟動目標 "任務".

4.2.2 集成測驗的測驗資料

我們通過對模塊間的轉換關系應用分支覆寫標準來選擇集成測驗資料，如圖4.3所示，圖4.4中的粗線代表了對 "任務 "模塊中的 "任務1 "單元應用分支覆寫標準的一個例子，如果 "Task1 "接收到一個 "SYS_ON=T "的信號，它就發出一個 "T1_TCB_RDY=T "的信號給內核模塊，然后，內核模塊發出一個'RUN_TSK1=T'信號來啟動'Task1'，

我們通過應用分支覆寫標準，考慮到衛星分解圖中的最終狀態，在內核模塊和任務模塊之間產生七個測驗資料，

4.3 系統測驗

系統測驗的目的是檢查它是否顯示出需求說明中描述的行為，在選擇系統測驗資料時，我們利用活動圖，選擇系統測驗資料的程式如下：

• (1) 從活動圖中提取場景，

• (2) 根據場景繪制序列圖，

  • 活動圖的一個模塊可以是序列圖的一個類，
  • 活動圖的事件和資料可以是序列圖的訊息，

• (3) 根據序列的資料流確定輸入資料，選擇系統測驗資料，

4.3.1 場景

從活動圖中提取的場景可以根據中斷條件進行分類，這里，我們從沒有中斷的例子中生成測驗資料，

4.3.2 順序圖

我們在活動圖的基礎上構成順序圖，如圖4.5所示，

4.3.2 系統測驗資料的選擇

我們根據順序圖中的資料流，通過識別輸入資料來選擇系統測驗資料，一種情況如圖4.5所示，輸入資料被顯示為一組信號： SYS_ON，和T1_TCB_RDY ~ T4_TCB_RDY，可以形式化為如下：
系統測驗資料 = (SYS_ON, T1_TCB_RDY, T2_TCB_RDY, T3_TCB_RDY,T4_TCB_RDY)
如果沒有中斷，總共有16個系統測驗資料，如表4.3所示，如果選擇定義為(T,F,T,T,T)的第15個系統測驗資料，預期輸出將是啟動 "任務6"，

嵌入式系統測驗

5.1 系統規范

在前面的章節中，我們展示了包括安全關鍵應用的RTOS軟體驗證在內的開發程式，在本節中，我們展示了測驗，以確定當它被嵌入到硬體中時是否作業良好，同時也檢查當它與應用軟體集成時是否有任何錯誤，測驗板是為此目的而設定的，所用的測驗板有一個英特爾80C196kc CPU，有RS-232埠作為介面，由于開發的PLC是針對數字植物保護系統（DPPS）的，我們對簡化的DPPS功能進行建模，并自動生成代碼，與RTOS軟體的程式相同，
DPPS接收每個變數的四個冗余輸入，然后，將它們與定義的設定點進行比較，當輸入超過設定點時，它產生 "真 "值作為輸出，結果被傳送到下一個模塊，在那里收集每四個冗余通道的結果，如果四個監測變數中有兩個以上的值顯示為 "真"，那么它就會發出一個跳閘信號，啟動保護功能，DPPS系統軟體被簡化，為了方便嵌入式系統測驗，只對一個監測變數進行建模，

5.2 可靠性評估

結論

在這項作業中，我們展示了為安全關鍵的核應用指定、驗證和測驗實時作業系統的整體程式，對實時作業系統的要求進行了分析，得出的結論是可以驗證的，因為實時作業系統所需的功能是簡單和確定的，在驗證之后，軟體被自動生成C語言，這個生成的代碼被測驗用于每個目的，單元測驗、集成測驗和系統測驗作為軟體測驗被執行，在單元測驗中，我們進行了兩種型別的測驗；一種是基于代碼的測驗，看是否有任何錯誤，另一種是基于狀態的測驗，檢查開發的軟體是否滿足驗證模型的屬性，在集成測驗中，我們制定了狀態組合圖，并通過應用分支覆寫標準生成測驗資料，在這個測驗中，我們檢查任何兩個或更多的模塊是否像我們在模型中設計的那樣正常通信，在系統測驗中，我們從需求規范中提取場景來檢查整個系統的行為，在驗證和測驗之后，我們將嵌入式系統作為一個原型來實作，我們生成簡化的應用軟體嵌入到RTOS中，然后測驗整個嵌入式系統，檢查它在與應用軟體和硬體集成時是否正常作業，我們計算出滿足可靠性標準所需的測驗次數，這將給我們帶來量化的可靠性，

標籤：其他

上一篇：讀改變未來的九大演算法筆記07_搜索引擎

下一篇：返回列表