基于模型檢查的嵌入式軟件構件化分析與驗證

聶捷楠

摘 要： 對嵌入式軟件構件化進行準確分析與驗證，能夠為嵌入式系統安全、穩定的運行提供保障。提出一種基于模型檢查的嵌入式軟件構件化分析與驗證方法。設計一種用于檢查軟件構件的模型，為嵌入式軟件構件化分析與驗證提供理論基礎；將嵌入式軟件系統模型用SMV語言的形式表達，利用SMV模型檢查工具實現對嵌入式軟件運行狀態的分析與檢驗。實驗結果表明，該模型能夠對嵌入式軟件構件化的非功能性方面的設計要求進行準確分析與驗證，為嵌入式系統安全穩定的運行提供了保障。

關鍵詞： 模型檢查； 嵌入式軟件； 構件化； SMV

中圖分類號： TN911?34； TP391 文獻標識碼： A 文章編號： 1004?373X（2016）24?0063?03

Embedded software component analysis and verification based on model checking

NIE Jienan

（Institute of Humanity Information Management， Chengdu Medical College， Chengdu 610500， China）

Abstract： The embedded software component is analyzed and validated accurately， which may provide the safe and stable operation for the embedded system. A analysis and validation method of the embedded software component based on model checking is put forward. A kind of model used to examine the software component is designed， which provides a theoretical foundation for analysis and verification of the embedded software component. The embedded software system model is expressed in the form of SMV language. The SMV model checking tool is used to implement analysis and test of the embedded software running status. The experimental results show that the model can accurately analyze and validate the non?functional design requirements of the embedded software component， and provided the safeguard for the embedded system safe and stable operation.

Keywords： model checking； embedded software； component； SMV

嵌入式系統各種功能的實現都離不開軟件[1]，軟件具有極其重要的意義[2]，它是影響嵌入式系統穩定運行的關鍵因素，一旦關鍵部位中嵌入式系統的軟件失效[3]，輕則造成財產損失，重則使生命受到威脅[4]。與PC機中的軟件相比，嵌入式系統中的軟件既要滿足其功能性設計要求[5]，又要滿足其非功能性的設計要求，如軟件的驅動程度、運算資源的占用程度、對能量的消耗程度等[6]。因此如何對嵌入式系統中的非功能性設計要求進行分析與驗證，已經成為當前IT領域中的一個熱點研究課題，受到專家學者的廣泛關注[7]。

目前，主要的嵌入式系統軟件驗證方法包括基于馬爾科夫的驗證方法[8]、基于定理證明的驗證方法和基于調試代理軟件的驗證方法[9]。最常用的是基于馬爾科夫的嵌入式軟件驗證方法。但利用傳統方法進行嵌入式系統軟件的驗證，驗證的項目主要為軟件的功能性設計要求，并且只能在軟件設計的后期才能進行驗證，難以對非功能性的設計要求進行準確分析與驗證，導致嵌入式軟件的穩定性與安全性難以得到保障[10]。

針對傳統方法存在的缺陷，提出一種基于模型檢查的嵌入式軟件構件化分析與驗證方法。利用SMV檢查工具對嵌入式軟件運行狀態進行分析與檢驗，實現對嵌入式軟件的分析與驗證。仿真實驗證明了改進算法在嵌入式軟件構件化分析與驗證方面的優勢。

1 嵌入式軟件構件化驗證模型設計

對嵌入式系統中的軟件進行構件化驗證，主要通過重復使用模塊化軟件來建立嵌入式軟件構件化驗證的模型，實現對嵌入式系統軟件的驗證。

通常情況下，一個完整的嵌入式系統軟件包括多個子系統軟件，其軟件系統具有較高的構件化特征。對嵌入式系統中構件化軟件進行分析與驗證，能夠為嵌入式系統安全穩定的運行提供保障。由于分析與驗證過程需要消耗大量能量，能量成為嵌入式系統中一種特殊的資源消耗，嵌入式系統的運行時間與能量消耗呈正相關，運行時間越長，能量消耗越多。因此，可以利用能量消耗的時間特性對嵌入式軟件構件化的驗證過程建模。

設計一種驗證模型，在驗證模型中加入嵌入式系統主要可以利用資源（包括存儲空間、緩沖區、消息隊列、傳感器）特征向量，使該模型能夠反映嵌入式軟件構件運行時主要可以利用資源的變化情況。設計驗證模型時需要包含如下參數：假設[VP]是資源利用狀態的集合，對于每一嵌入式資源利用狀態都有[vi∈VP]，且[P]的初始狀態為[vi∈VInitP]；[FP]為資源狀態的映射集合，[FP=（f1P，f2P，…，fKP）]，其中[K]為嵌入式系統中可利用資源種類的數目；[WP]表示可利用資源的有窮集合，[WP=（VP，FP（VP））]；[ΓP]為資源利用狀態的轉換集。通過以上參數的描述，將嵌入式軟件構件化驗證的模型轉化為多元組的形式進行構建：

[P=VP?FP?WP?ΓP]

2 嵌入式軟件構件化驗證方法設計與實現

本文構建立了嵌入式軟件構件化驗證的模型，將嵌入式軟件構件化驗證模型中軟件運行路徑逐一遍歷，直到獲取正確的軟件運行路徑，實現模型檢查算法設計，最終實現基于模型檢查的嵌入式軟件構件化分析與驗證。

2.1 基于時序邏輯CTL算子的模型檢查算法

首先獲得嵌入式軟件運行過程中的時序邏輯CTL算子，通過CTL算子獲取嵌入式軟件構件化驗證模型中軟件運行路徑的有關性質，并逐一遍歷，直到搜索出正確的軟件運行路徑，設計了模型檢查算法。具體過程如下所述：將時序邏輯CTL劃分為分支時間算子和線性時間算子。其中，分支時間算子包括軟件的全部運行路徑A和特定的運行路徑E，線性時間算子包括G（always，經常）、F（sometimes，偶爾）、X（next time，下一時刻）和U（until，直到）。引入上述構建的嵌入式軟件構件化驗證模型，利用時序邏輯CTL中的分支時間算子和線性時間算子描述嵌入式軟件構件化驗證模型中軟件運行路徑的相關性質，如圖1所示。圖1（a）為[EFg]，表示“資源利用狀態的集合[VP]中存在一條運行路徑使布爾量公式[g]在某種運行狀態下為真”；圖1（b）為[AFg]，表示“資源狀態的映射集合[FP]中所有運行路徑中布爾量公式[g]在某種運行狀態下為真”；圖1（c）為[EGg]，表示“可利用資源的有窮集合[WP]中存在一條運算路徑使得布爾量公式[g]在該路徑中的全部狀態下都為真”；圖1（d）為[AGg]，表示“資源利用狀態的轉換集[ΓP]中布爾量公式[g]在全部運行路徑中的全部狀態下都為真”，通過對這些條件進行逐一判定，最終選擇正確的軟件運行路徑，完成模型檢查算法設計。

2.2 基于模型檢查的嵌入式軟件驗證的實現

針對嵌入式軟件進行分析與驗證的模型檢查工具主要包括：貝爾實驗室開發的SPIN工具、赫爾辛基工業大學開發的PROD工具、CMU大學開發的SMV工具等。每種模型檢查工具都有不同的特點，其中，SMV工具結構簡單、運算量小、準確率高。因此本文將SMV工具作為嵌入式軟件分析與驗證的模型檢查工具。

SMV工具是根據“符號模型檢查”的原理開發，目的是通過對符號模型對軟件的性能進行檢查，隨著SMV工具功能的不斷完善，SMV工具已經被廣泛應用于軟件有限狀態的檢查。本節將上述模型檢查算法利用SMV語言的形式表達，構建SMV模型檢查工具，完成嵌入式軟件構件化分析與驗證，具體步驟如下所述：

一個完整的SMV模型檢查工具由兩個部分構成，分別為：一個狀態轉換系統；一個CTL公式組，能夠準確描述嵌入式軟件的屬性。通過這兩個部分可以將嵌入式軟件的構件化驗證過程描述為一個二叉樹BDD的形式。SMV模型檢查工具只需要對嵌入式軟件二叉樹BDD的運行狀態進行搜索，將搜索結果進行逐一判定，判定后輸出的結果分為：正確和錯誤，即為模型檢查算法對嵌入式軟件構件化的驗證結果，實現了嵌入式軟件的構件化驗證。

2.3 部分代碼設計

利用SMV模型檢查工具對嵌入式系統的構件化進行驗證與分析，部分程序如下所述：

MODULE main

VAR

Pen_irq；booleam；

D_jitery_delay；boolean；

U_jittery_delay；boolean；

Detect：touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）；

SPEC

AG（detect，state=Touch_up&pen_irq=0?>AF detect，state=Touch_Down）

SPEC

AG（detect，state=Touch_Down&pen_irq?>AF detect，state=Touch_up）

MODULE Touch_Detect（pen_irq，d_jittery_delay，u_jittery_delay）

state：{ Touch_Idle，Touch_up，Touch_down，Touch_ChkUp；Touch_chkDown；}

3 實驗結果及分析

3.1 實驗環境設置

為了驗證改進算法在嵌入式軟件構件化驗證方面的有效性，需要進行仿真實驗。嵌入式軟件構件化分析與驗證的運行環境為：Windows 7操作系統，利用Rational Rose 2003生成 MDL文件；以嵌入式軟件的非功能性設計要求為依據，對改進算法和傳統算法的性能進行比較。研究表明，資源的占用程度、投影路徑中非法信息檢驗、能耗行為的路徑是嵌入式軟件構件化的具體屬性，本文以手持PDA為例，以這三個屬性為目標，對手持PDA軟件進行構件化驗證。

3.2 不同算法下仿真實驗結果及分析

首先利用上述獲得的SMV模型檢查工具對PDA的通信的驅動程序和信息交互序列的驅動程序運行資源的占用情況進行檢驗。這兩種驅動程序包含三類資源，分別為r1，r2和r3，軟件在進行狀態轉換過程中需要占用的資源數量和資源種類利用向量進行描述，例如，

3.2.1 不同算法下嵌入式軟件運行資源的占用情況驗證

首先利用不同算法對手持PDA軟件進行資源的占用情況方面驗證，以驗證軟件在狀態轉換的過程中需要占用的資源是否滿足設計要求。利用傳統算法進行驗證結果表明：傳統算法只能檢測出軟件在狀態轉換的過程中需要占用的資源種類為3種，但不能檢測出具體的資源名稱和占用資源的數量；而利用改進算法進行驗證結果表明：手持PDA通信的驅動程序在進行轉換的過程中有一個資源處于非法狀態，即（s4|s1），該程序在進行狀態轉換的過程中需要的資源為[r1，2]，[r2，5]，[r3，3]。（s4|s1）狀態在轉換的過程中對資源r2的需求量為5，而在實際程序中r2的資源總的數量為4，因此可推出該狀態在轉換的過程中有1個資源不符合設計要求，體現了改進算法的巨大優勢。

3.2.2 不同算法下嵌入式軟件運行中投影路徑中非法

信息檢驗驗證

為了進一步驗證改進算法的有效性，本文以PDA中信息交互序列的驅動程序為例，對信息交互過程中投影路徑中的非法信息進行檢驗。結果表明，利用傳統算法進行投影路徑中非法信息檢驗，沒有搜索出對應的投影路徑中存在的非法信息；而改進算法結果表明：PDA在進行信息交互的過程中，在組合狀態空間內存在一個與信息交互行為相對應的投影路徑，但是該路徑存在一個非法狀態（s2|s1），占用資源[r2，r3]，表明在此信息交互行為的狀態下，嵌入式軟件系統不滿足設定的資源限制條件，需要PDA軟件的編寫者對軟件進行及時修改，以保證嵌入式軟件的安全性。嵌入式軟件的非法信息驗證界面如圖2所示。

3.2.3 不同算法下嵌入式軟件運行中能耗行為的路徑

比對驗證

在PDA中，為了對比不同算法在嵌入式軟件能耗行為的路徑方面的驗證性能。利用不同算法對PDA非功能性的能耗行為的路徑進行檢驗。首先搜索出滿足非功能性行為的路徑共19條。然后利用不同算法對這19條路徑消耗的能耗進行對比。

實驗結果為：實際情況下所有有路徑中最大能量為44.6，對應的投影路徑為s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8，改進算法下所有路徑中最大能量為46.3，對應的投影路徑為s0|s0（0，0）2.9→s1|s1（0，0）5.5→s2|s1（0，2）4.1→s3|s1（0，4）5.4→s4|s1（0，7）5.6→s5|s1（0，9）4.8；傳統算法下最大能量為29.7，對應的投影路徑為s0|s0（0，0）2.8→s1|s1（0，0）5.5→s2|s1（0，1）4.0→s3|s1（0，3）5.3→s4|s1（0，5）5.3→s5|s1（0，9）4.7。通過仿真實驗表明，傳統算法與實際的能耗值相差較大，并且對應的投影路徑不一致；而改進算法與實際的能耗最為接近，并且對應的投影路徑一致，充分體現了改進算法在嵌入式軟件能耗行為的路徑設計驗證方面的優越性。

4 結 語

針對傳統算法存在的缺陷，提出一種基于模型檢查的嵌入式軟件構件化分析與驗證方法。利用SMV檢查工具對嵌入式軟件運行狀態進行分析與檢驗，實現對嵌入式軟件的分析與驗證。仿真表明，改進算法能夠對嵌入式軟件構件化的非功能性方面的設計要求進行準確分析與驗證，為嵌入式系統安全穩定的運行提供了保障。

參考文獻

[1] 王鋒，張弛.構件化嵌入式軟件設計模型驗證工具的研究[J].通訊世界，2014（21）：36.

[2] 王博，白曉穎，賀飛.可組合嵌入式軟件建模與驗證技術研究綜述[J].軟件學報，2014，25（2）：234?253.

[3] 符寧，杜承烈，李建良，等.AADL分級調度模型的分析與驗證[J].計算機研究與發展，2015，52（1）：167?176.

[4] 胡寧，葉宏.嵌入式操作系統的形式化驗證方法[J].航空計算技術，2015（2）：96?100.

[5] 白海洋，李靜，趙娜.基于時間自動機的嵌入式軟件模型可調度性驗證[J].計算機工程與科學，2013，35（3）：121?127.

[6] 趙競雄.嵌入式系統威脅與風險評估過程仿真分析[J].計算機仿真，2014，31（4）：295?298.

[7] 黃傳林，黃志球，胡軍，等.基于擴展SysML活動圖的嵌入式系統設計安全性驗證方法研究[J].小型微型計算機系統，2015（3）：408?417.

[8] 謝開斌，陳海明，崔莉.物聯網軟件體系結構中的感執模型的求精[J].軟件學報，2014，25（8）：1659?1670.

[9] 王誠.硬件構件化的嵌入式底層構件開發技術分析[J].中國科技博覽，2013（9）：134.

[10] 黃菲.嵌入式實時軟件的構件化開發技術探究[J].信息技術與信息化，2015（10）：197?198.