基于元模型的Simulink靜態(tài)分析技術

摘 要： 為解決目前Simulink模型規(guī)則檢查工具對國內(nèi)如飛行控制等一些特定領域的標準規(guī)范覆蓋不完善的問題，設計了41條建模準則，并基于元模型理論，提出了一種共性的解析和檢查框架，在此基礎上實現(xiàn)了Simulink模型規(guī)則檢查工具SimREG。該方法通過一種無編譯的方式來實現(xiàn)對Simulink模型的靜態(tài)規(guī)則檢查，在Simulink模型到元模型的映射過程中提取針對每條準則執(zhí)行檢查時需要的模型信息，并將模型重構(gòu)為有向圖的形式，然后在遍歷過程中，對圖中每個節(jié)點進行選定準則的分析處理，完成檢查過程。SimREG完成了全部41條建模準則的檢查過程，在與三個有代表性的規(guī)則檢查工具的對比實驗中取得了更好的檢查結(jié)果。SimREG工具將元模型理論應用于Simulink模型的規(guī)則檢查過程中，在檢查速度更快的同時獲得了更低的漏報率和誤報率。

關鍵詞： Simulink模型； Stateflow模型； 元模型； 靜態(tài)規(guī)則檢查

中圖分類號： TP311.5"" 文獻標志碼： A

文章編號： 1001-3695（2022）01-036-0206-08

doi：10.19734/j.issn.1001-3695.2021.05.0225

Simulink static analysis technology based on metamodel

Wang Rui1，2， Chen Jing2， Wang Kunlong2， Zheng Yifan2， Ke Wenjun2，3，4， Zhong Jilong5

（1.Graduate School of the Second Research Institute of China Aerospace Science amp; Industry Corporation， Beijing 100854， China; 2.Beijing Institute of Computer Technology amp; Applications， Beijing 100089， China; 3.Institute of Computing Technology， Chinese Academy of Sciences， Beijing 100190， China; 4.University of Chinese Academy of Sciences， Beijing 100049， China; 5.National Institute of Defense Technology Innovation， PLA Academy of Military Science， Beijing 100091， China）

Abstract： Current Simulink-rule-checking tools cannot fully cover the criteria and specifications of some specific fields such as flight control. To address this issue， this paper firstly designed 41 modeling criteria， then proposed a common parsing and checking framework based on the metamodel theory， and implemented a checking the Simulink model rules tool SimREG. Besides introducing a non-compiler way to static rule checking on Simulink model， SimREG extracted the model information for checking each criterion during mapping the Simulink model to the metamodel， and reconstructed the model into a directed graph. Furthermore， in the traversal process， each node in the directed graph was analyzed and processed by the selected criteria to complete the inspection process. The checking process for all 41 modeling criteria was also addressed through SimREG. Finally， in the experiment compared with 3 representative rule checking tools， SimREG obtained a preferable results. By applying metamodel theory to the rule checking process of Simulink model， SimREG gets a faster inspection speed， a lower 1-negative rate， and a lower 1-positive rate.

Key words： Simulink model; Stateflow model; meta-model; static rule checking

0 引言

質(zhì)量是軟件的生命［1］，軟件質(zhì)量出現(xiàn)問題，輕則造成財產(chǎn)損失，重則威脅人們的生命。在航空航天、汽車電子等領域，嵌入式軟件廣泛應用。在這些領域，嵌入式軟件大都采用C語言開發(fā)，使用大量的數(shù)據(jù)結(jié)構(gòu)和指針，涉及復雜的數(shù)值運算，針對復雜的功能還會采用多任務并行方式設計［2］，保證軟件的質(zhì)量十分困難。當這些軟件的質(zhì)量出現(xiàn)問題時，極有可能引發(fā)災難性的后果，因此這些領域?qū)浖|(zhì)量有著極高的要求［3］。

為了保證軟件的質(zhì)量，人們提出了許多編程規(guī)范來約束開發(fā)過程，如Misra C［4］、ISO 26262［5］、Effective C++［6］、DO-178B［7］等。同時，針對這些標準規(guī)范設計了靜態(tài)規(guī)則檢查工具來完成對編碼合規(guī)性的檢查。根據(jù)檢查過程是否需要對代碼進行編譯，靜態(tài)規(guī)則檢查工具可以分為無編譯的和基于編譯的兩類。其中無編譯的工具，如QAC、Splint，具有較高的適應性和較快的檢查速度，但準確率相對較低；基于編譯的工具，如Testbed、Klocwork等，對編譯過程產(chǎn)生的中間文件進行分析，檢查速度較慢，但準確率能夠得到較大的提高［8］。

為了適應大規(guī)模復雜軟件的開發(fā)需求，模型驅(qū)動的軟件開發(fā)（model-driven development，MDD）作為傳統(tǒng)的代碼開發(fā)方法的一個替代方式，在嵌入式軟件開發(fā)領域得到廣泛應用［9］。通過模型開發(fā)、仿真驗證和自動代碼生成，可有效解決大規(guī)模嵌入式軟件開發(fā)的效率、成本與質(zhì)量問題［10］。其中，MATLAB/Simulink作為一種成熟的模型開發(fā)工具已經(jīng)被廣泛應用于航空工業(yè)、汽車電子等眾多領域［11］ 。本文對GitHub上不同領域的嵌入式軟件項目進行了統(tǒng)計，圖1顯示了使用C語言和MATLAB/Simulink所開發(fā)項目的統(tǒng)計結(jié)果，可以看到，已經(jīng)有很大比例的嵌入式軟件使用了MATLAB/Simulink進行開發(fā)，尤其在雷達系統(tǒng)上，MATLAB/Simulink的使用率已經(jīng)高于C語言。在國際上，Simulink模型已經(jīng)應用于獵戶座飛船的GNamp;C算法［12］、 A380 飛機的燃油控制系統(tǒng)［13］、梅賽德斯奔馳卡車的巡航控制器［14］等開發(fā)中。在國內(nèi)，Simulink在濰柴動力的柴油發(fā)動機ECU 軟件［15］、東風混合動力電動汽車的電池管理系統(tǒng)［16］等設計開發(fā)中得到了應用。

對于Simulink的建模過程，也形成了一些建模準則，如MAAB［17］、JMAAB［18］、MAB［19］等。在規(guī)則檢查方面，目前應用最廣泛的是MathWorks公司的Model Advisor工具，該工具能夠?qū)崿F(xiàn)對指定規(guī)則的檢查，并幫助設計人員對發(fā)現(xiàn)的問題進行修正，但Model Advisor對國內(nèi)一些特定領域的執(zhí)行規(guī)范覆蓋并不完善，而且檢查過程通常需要對模型進行編譯，但實際應用中經(jīng)常需要對暫時無法完成編譯的模型進行檢測。

本文基于元模型提出了一種無編譯的方法來實現(xiàn)對Simulink模型的靜態(tài)規(guī)則檢查。首先通過對Simulink建模元素的特征進行提取，構(gòu)建元模型以對Simulink模型進行抽象表示;其次，在實現(xiàn)Simulink模型到元模型的映射過程中提取規(guī)則檢查需要的模型信息;然后，利用這些信息針對每條準則設計專門的規(guī)則檢查腳本;最終實現(xiàn)對Simulink模型的規(guī)則檢查。本文針對國內(nèi)軍用領域的GJB 8114標準［20］，提出了一系列與代碼生成相關的建模準則作為規(guī)則檢查過程的依據(jù)，并實現(xiàn)了相關檢查過程。在數(shù)據(jù)集上的實驗結(jié)果表明，本文方法相比于廣泛使用的Simulink規(guī)則檢查工具Model Advisor及其他兩個基于元模型SLDG［21］和Massif［22］實現(xiàn)的工具，具有更好的檢查效果。

1 相關工作

1.1 Simulink模型

使用Simulink時，用戶通過連接各種不同功能的模塊，并對模塊參數(shù)進行配置來構(gòu)建軟件系統(tǒng)模型［23］，用于嵌入式軟件的控制律設計等場景。Simulink中的模塊大致有信號源、信號處理和信號接收三種類型。其中，信號源模塊用來向模型提供輸入信號，如in、constant、clock等；信號處理模塊接收來自其他模塊的信號輸入，進行處理后輸出信號，如product、logical operator、integrator等；信號接收模塊用來接收模型的輸出信號，如outport、date store write、to file等。如圖2所示，模型從in1和constant模塊獲得輸入，經(jīng)過operator模塊的相等判斷后，將結(jié)果輸出到out1模塊。

如果軟件中包含系統(tǒng)狀態(tài)轉(zhuǎn)換的過程，可以使用Chart模塊在Simulink中嵌入Stateflow模型，通過有限狀態(tài)機對軟件系統(tǒng)中的時序和組合邏輯進行建模仿真［23］。Stateflow模型主要由狀態(tài)（state）、節(jié)點（junction）和轉(zhuǎn)換（transition）三部分構(gòu)成。其中，狀態(tài)（state）表示系統(tǒng)在滿足某種條件時可到達的一個狀態(tài)及可能執(zhí)行的一些操作；節(jié)點（junction）表示需要作出決策的點，它將決策過程劃分為多個階段；轉(zhuǎn)換（transition）是狀態(tài)或節(jié)點之間遷移的路徑，包含了遷移時需要的條件或執(zhí)行的動作等信息。圖3所示的Stateflow模型中包含了兩個狀態(tài)和兩個節(jié)點以及連接它們的轉(zhuǎn)換。

1.2 軟件靜態(tài)規(guī)則檢查技術

靜態(tài)規(guī)則檢查作為一種軟件靜態(tài)分析過程中的基本測試手段，能夠在開發(fā)早期發(fā)現(xiàn)軟件錯誤，對縮短軟件開發(fā)周期、保證軟件質(zhì)量、降低開發(fā)成本起著關鍵作用。根據(jù)在靜態(tài)規(guī)則檢查過程中是否需要對代碼進行編譯，可以將檢查方法分為基于編譯過程中間結(jié)果的方法和無編譯的方法［24］，其執(zhí)行過程如圖4所示。

其中，基于編譯的方法通常是對編譯中的過程文件進行分析。常用工具LDRA Testbed是英國Liverpool數(shù)據(jù)研究會開發(fā)的程序設計規(guī)則檢查工具［25～27］，檢查過程需要對源代碼進行詞法分析和語法分析并構(gòu)建AST樹，可以對C、C++、Ada等語言進行程序設計規(guī)則檢查，并且支持 MISRA C/C++/Ada 標準，支持的規(guī)則約有200多條。部分場景下，對代碼片段執(zhí)行檢查或無法搭建完整的編譯平臺時，需要進行無編譯的規(guī)則檢查，直接對程序源代碼進行分析，沒有編譯處理過程。英國PRQA公司開發(fā)的代碼靜態(tài)分析工具QAC，處于靜態(tài)編程規(guī)則檢查領域的領先地位，其內(nèi)置了1 025條規(guī)則，在汽車、通信、航空航天等領域擁有大量的用戶。QAC 在分析代碼時，并不對代碼進行編譯，只是分析程序時要用到一些編譯器的信息，如編譯器頭文件、宏以及嵌入式的CPU設置等［28］。

在采用Simulink模型進行軟件開發(fā)時，應用最廣泛的規(guī)則檢查工具是Simulink自帶的Model Advisor。Model Advisor工具自帶200多條檢查規(guī)則，為MAAB［17］、JMAAB［18］等國外常用建模規(guī)范提供支撐［29］。但一方面，Model Advisor工具主要用于商用領域的Simulink模型規(guī)則檢查，尤其是在汽車電子方面，對國家軍用標準的支持力度較弱，而且對包含Stateflow的模型執(zhí)行檢查時，其檢查效果差強人意。另一方面，Model Advisor工具在檢查過程中通常需要花費較多的時間對模型進行編譯，而在Simulink模型開發(fā)過程中需要對無法完成編譯的模型進行檢查，導致規(guī)則檢查失敗。

1.3 元模型技術

元模型是模型驅(qū)動軟件開發(fā)的一個核心內(nèi)容，其定義了組成模型的元素和元素之間的關系。元模型作為描述模型而產(chǎn)生的“抽象語言”，可為模型的解析與處理提供有效支撐。統(tǒng)一建模語言UML和系統(tǒng)建模語言SysML已經(jīng)被OMG國際組織定義了標準元模型［30，31］。同時，一些學者面向特定任務，研究設計了Simulink元模型，用于輔助分析模型的控制流和數(shù)據(jù)流等信息。具體的，文獻［32］設計了一種Simulink元模型，通過在此基礎上設計的轉(zhuǎn)換規(guī)則，完成基于DoDAF框架實現(xiàn)的架構(gòu)模型到Simulink模型的自動轉(zhuǎn)換；文獻［33］提出了Simulink分析和轉(zhuǎn)換環(huán)境MATE，利用元建模技術和可視化圖形轉(zhuǎn)換來根據(jù)指定準則自動分析和校正模型，并且能夠?qū)δＰ瓦M行控制流和數(shù)據(jù)流分析；Prasad等人［21］設計了一個Simulink元模型SLDG用于捕獲模型中存在的各種類型的依賴關系，并應用到模型更改點的影響域分析及回歸測試的用例篩選中；Son等人［34］通過定義元模型，實現(xiàn)了從Simulink模型到電子商務模型ECML的轉(zhuǎn)換；Simulink集成框架Massif［22］定義了一個EMF元模型來描述Simulink建模功能，將Simulink模型轉(zhuǎn)換為Eclipse-EMF模型，通過提供與EMF之間的導入和導出功能來支持對MATLAB Simulink模型的處理。為了實現(xiàn)Simulink模型的規(guī)則檢查，本文設計了一個元模型來對Simulink模型進行分析，并基于GJB 8114標準［20］提出了41條Simulink建模準則用于指導建模過程，針對提出的建模準則，設計和實現(xiàn)了相關的規(guī)則檢查腳本，為模型的規(guī)范符合性檢查提供支持。

2 方法

2.1 問題形式化

下面給出模型規(guī)則檢查任務的定義：給定一個模型M={B，E}，其中，B={B1，…，Bn}表示模型中使用的模塊集合，E={（Bi，Bj）|Bi，Bj∈B}表示連接各模塊的信號線集合，（Bi，Bj）表示模塊Bi和Bj之間有信號線相連。R={R1，…，Rm}為給定的建模準則集合。該任務的主要目標是對模型M中B和E的元素進行分析，以找到違反準則集合R中任意準則的模型元素，并使用Q={Ml，Rl}的集合Q返回元素位置以及違反的準則，其中，Ml∈B∪E為違反準則的元素，Rl∈R為該元素違反的準則。

2.2 方法框架

本文基于元模型理論針對Simulink模型設計了一種無編譯的規(guī)則檢查方法。首先根據(jù)設計的建模規(guī)則提出了一個元模型來抽取Simulink模型信息；然后設計并實現(xiàn)了一種Simulink模型到元模型的映射方法；最后在對建立的元模型映射進行遍歷的同時執(zhí)行本文設計的規(guī)則檢查腳本，輸出檢查結(jié)果。檢查結(jié)果包含了違反的準則和問題的位置，以方便檢測人員實現(xiàn)對問題的快速定位和確認。規(guī)則檢查方法框架如圖5所示。

2.3 Simulink元模型

2.3.1 元模型設計

本文針對Simulink模型的規(guī)則檢查問題，提出了一個元模型來對Simulink模型中的各個元素和這些元素之間的關系進行抽象表示。通過元模型實現(xiàn)對要檢查的Simulink模型的解析，根據(jù)檢查規(guī)則的約束，將不同元素進行不同級別的抽象，并抽取出規(guī)則檢查過程中需要的模型關鍵信息，如模塊的類型、輸入信號的類型、執(zhí)行的操作等。所設計的元模型部分結(jié)構(gòu)如圖6所示。

在本文設計的元模型中，node類是所有元素的基類，包含type、SID等屬性。node類主要包括四個子類：

a）狀態(tài)流圖（Stateflow）是Simulink模型中嵌入的Stateflow模型的抽象，包含狀態(tài)（state）、節(jié)點（junction）和轉(zhuǎn)換（transition）三個主要的子類，分別代表了構(gòu)建Stateflow模型需要的三種元素。

b）模塊（block）是對Simulink模塊庫中提供的用于構(gòu)建Simulink模型的各種模塊的一個抽象，是Simulink模型的基本元素。block類的子類chart是Stateflow模型對應模塊的抽象。block類的另一個子類subsystem代表了Simulink模型中的一類特殊模塊，該模塊內(nèi)部嵌套了Simulink模型的一個子模型，與Simulink模型具有相同的結(jié)構(gòu)，用于實現(xiàn)一個特定的功能。

c）接口（port）是構(gòu)成Simulink模型的模塊跟外界進行交互接口的抽象，需要對接口的類型、接口變量的數(shù)據(jù)類型、接口是否被連接等信息進行存儲。

d）連線（line）是Simulink模型中連接各個模塊的信號線的一個抽象，對信號線的信號名稱、連接的模塊及接口等信息進行存儲。

2.3.2 模型到元模型的映射

在Simulink模型到元模型的映射過程中，要完成規(guī)則檢查所需關鍵信息的提取，需要對模型中的每一個元素進行處理，在向元模型的映射過程中構(gòu)建相應的節(jié)點，并建立節(jié)點間的鄰接關系，最終以有向圖的形式將原始的Simulink模型表示出來。在完成Simulink模型到元模型的映射時，需要將模型分為對Simulink模型中模塊的處理和對模型包含的Stateflow模型內(nèi)部結(jié)構(gòu)的處理兩部分，其映射規(guī)則如表1所示。為了建立Simulink模型到元模型的映射，需要迭代處理模型中的所有模塊。本文通過廣度優(yōu)先的方式遍歷模型中的每一個模塊，根據(jù)模塊的不同類型建立相應的元模型映射節(jié)點，并保存不同的模塊信息，在完成模塊節(jié)點的建立后，建立該模塊的端口節(jié)點及輸出信號對應連線的節(jié)點，并更新它們的鄰接信息。如果遍歷到的當前模塊為chart類型模塊，則表示模型嵌入了一個Stateflow模型，需要建立該Stateflow模型中元素對應的state、junction、transition類型節(jié)點，并完善它們之間的鄰接關系。Simulink模型到元模型映射過程如算法MetaModel_Construct所示。

算法1 MetaModel_Construct 算法

輸入：M_Path為Simulink模型的本地路徑。

輸出：M_Meta={N1，N2，…，Nn}為Simulink模型的元模型表示節(jié)點集合。

B={B1，B2，…，Bm|Bi∈findblock（M_Path）}

//加載模型，并獲取模型的模塊集合B

for Bi in B //對模塊集合B中的每一個模塊Bi進行處理

if indegree（Bi）=0//若模塊Bi沒有輸入信號

Bi→S //將模塊Bi加入隊列S

repeat： //重復下述過程

S→Bk //從隊列S取出一個模塊

M_Meta←creat_BIOL（Bk）

//建立模塊Bk、Bk接口及輸出信號線的元模型節(jié)點

S←{Bkj|Bkj adjacent to Bk}

//與模塊Bk輸出接口相連的模塊Bkj加入隊列

update_adj（M_Meta） //更新鄰接關系

if Bk is SF //模塊包含Stateflow

M_Meta←creat_SF（Bk） //構(gòu)建對應元模型

until S= //S非空時重復上述過程

其中，findblock調(diào)用MATLAB函數(shù)load_system加載Simulink模型并通過find_system函數(shù)獲取模型中所有的塊。 creat_BIOL函數(shù)實現(xiàn)模型元素到元模型的映射過程，通過MATLAB函數(shù)get_param提取模塊中的關鍵信息，建立對應元模型的元素節(jié)點，并在之后的函數(shù)update_adj中，完善元素節(jié)點之間的鄰接關系，如模塊鄰接點為該模塊輸出接口，輸出接口鄰接點為接口連線，連線鄰接點為連接的輸入接口，輸入接口鄰接點為所在模塊等。Simulink模型及其嵌套的Stateflow模型建立的元模型表示分別如圖7、8所示。圖7中Simulink模型的每一個模塊都映射了相應的一組節(jié)點，如模塊in1映射了節(jié)點（1，in1，B）、（2，-，Op）以及（3，-，L），括號內(nèi)的內(nèi)容分別為節(jié)點的序號、對應模型元素名稱、類型。圖8中Stateflow模型的每一個元素映射了一個相應的元模型節(jié)點，如state類型元素off映射了元模型節(jié)點（1，off，S）。

2.4 Simulink模型規(guī)則檢查

2.4.1 Simulink建模準則設計

目前已經(jīng)出現(xiàn)了一些針對Simulink的建模標準，如MAAB［17］、JMAAB［18］、MAB［19］等，但主要應用于汽車制造領域的嵌入式軟件開發(fā)。本文對軍用領域的建模需求進行分析，針對GJB 8114標準［20］設計了41條準則。其中，強制類準則25條，建議類準則16條。強制類準則是強制要求遵守的準則，建議類準則是建議遵守的準則。由于內(nèi)容限制，本文只列舉具有代表性的6條準則，如表2、3所示。

2.4.2 Simulink模型規(guī)則檢查

在2.3.2節(jié)中，本文介紹了Simulink模型到元模型的映射過程，將Simulink模型重構(gòu)為一個有向圖的形式，并且在有向圖的各個節(jié)點中存儲了規(guī)則檢查過程需要的模型信息，本文在此基礎上設計了Simulink模型的規(guī)則檢查過程。該有向圖中每個節(jié)點采用鄰接數(shù)組的形式存儲了與其相鄰的節(jié)點的編號。檢查過程采用深度優(yōu)先的方式對有向圖進行遍歷，在遍歷過程中遇到可能違反當前準則的有向圖節(jié)點時，則提取該節(jié)點包含的模型信息，通過對這些信息進行分析處理，確定該節(jié)點是否違反規(guī)則。由于每條準則的內(nèi)容不同，導致針對的檢查對象不同，對于不同的模型設計準則，需要設計不同的檢查算法。對此，基于元模型性理論，本文提出了一種共性的解析和檢查框架。基于該框架，本文完成了41條準則的檢查算法設計。

規(guī)則檢查過程調(diào)用Rule_Check算法實現(xiàn)，該算法以Simulink模型通過元模型映射成的有向圖M_Meta和待檢查的規(guī)則C′∈C為輸入，輸出檢查結(jié)果信息E_Set，該信息包含違反的規(guī)則、問題位置、問題描述等。Rule_Check算法第一步從有向圖序列獲取一個未訪問的節(jié)點Ni進行檢查，并將其鄰接點N_adj={Ni1，…，Nik}放入待檢查節(jié)點棧ST；第二步，對棧ST中的節(jié)點進行迭代，從棧中取出一個節(jié)點Nj進行檢查，并將其鄰接點N_adj={Nj1，…，Njl}放入待檢查節(jié)點棧ST，重復這一過程直到棧ST為空，返回第一步，若所有節(jié)點都被遍歷，算法結(jié)束。算法2以準則F_018（禁止對浮點數(shù)進行是否相等的比較）為例，對Simulink規(guī)則檢查框架進行描述。

算法2 Rule_Check算法

輸入：M_Meta={N1，N2，…，Nn}為當前已經(jīng)建立的元模型表示；C′∈C為待檢查的規(guī)則。

輸出：E_Set={E1，E2，…，Em}為規(guī)則檢查結(jié)果。

1 NS=［0，0，…，0］，ST={} //初始化節(jié)點訪問狀態(tài)NS和訪問棧ST

2 for Ni in M_Meta //對元模型表示中的每一個節(jié)點Ni進行處理

3 if NSi=0 //如果節(jié)點Ni未被訪問

4" Ni→ST //將節(jié)點Ni放入棧ST

5" repeat： //重復下述過程

6"" ST→Nj //從棧ST獲得一個節(jié)點Nj

7"" if class（Nj）=relational operator //如果節(jié)點Nj執(zhí)行比較操作

8""" if type（in1）=type（in2）=double

//如果節(jié)點Nj的輸入in1和in2都為浮點型

9"""" if operator（Nj）∈{==，！=，～=}

//如果節(jié)點Nj執(zhí)行判等操作

10""""" set（E） //節(jié)點Nj違反規(guī)則，設置問題信息E

11"" else if class（Nj）∈（S，T） //如果節(jié)點Nj類型是S或T

12""" OP=getoperator（Nj） //獲取節(jié)點Nj包含的操作OP

13""" if Operator（OP）∈{==，！=，～=}

//如果節(jié)點Nj執(zhí)行判等操作

14"""" ［a，b］=getvariate（OP） //獲取執(zhí)行操作的變量a，b

15"""" if type（a）=type（b）=double

//如果變量a，b都為浮點型

16""""" set（E） //節(jié)點Nj違反規(guī)則，設置問題信息E

17"" E_Set←E //將問題E放入檢查結(jié)果集

18"" NSj=1 //節(jié)點Nj標記為已訪問

19"" N_adj={Nk|NSk=0，Nk adjacent to Nj}

//獲取節(jié)點Nj未訪問的鄰接點集N_adj

20"" N_adj→ST //將鄰接點集N_adj入棧

21" until ST= //ST非空時執(zhí)行上述操作

其中，getoperator函數(shù)用于查看遍歷到的當前元素中是否包含判等操作，對于B類型元素執(zhí)行的操作可通過調(diào)用MATLAB函數(shù)get_param獲得；如果是S或T類型元素，則使用getoperator函數(shù)通過正則表達式進行相應操作字符的提取。getvariate函數(shù)用于提取遍歷到的當前元素操作的變量;B類型元素調(diào)用MATLAB函數(shù)get_param獲得;S或J類型元素使用正則表達式進行提取，然后通過之后的type函數(shù)進行是否是浮點型的判斷。如果當前元素Ni違反了規(guī)則，使用set函數(shù)設置規(guī)則違反信息，包括違反規(guī)則的元素、所在位置、違反的規(guī)則號等。

對于不同的準則，本文設計了不同的檢查算法，例如算法2中7～18行，對準則F_018進行檢查時對當前遍歷到的節(jié)點N進行判斷，如果節(jié)點N是relational operator類型模塊映射的節(jié)點，則提取節(jié)點N中包含的兩個輸入的數(shù)據(jù)類型和執(zhí)行的比較操作的信息，若輸入數(shù)據(jù)類型都為double型，且執(zhí)行等于或不等于操作，則對問題進行輸出；如果節(jié)點N是S或T類型節(jié)點，則將節(jié)點中包含操作信息的字符串與表示判等操作的字符串進行匹配，若匹配成功，則表示節(jié)點N執(zhí)行了判等操作，需要提取執(zhí)行判等的兩個變量的數(shù)據(jù)類型進行判定，數(shù)據(jù)類型都為double類型時，則對問題進行輸出。

2.4.3 應用舉例

本文基于2.4.2節(jié)介紹的規(guī)則檢查過程，實現(xiàn)了規(guī)則檢查工具SimREG。在這里本文實現(xiàn)了一個簡單的Simulink模型，來驗證該準則F_018的執(zhí)行效果，如圖9所示，名稱為Op的模塊為relational operator（關系運算）類型，且進行了浮點數(shù)的相等比較，違反了準則F_018，在檢查結(jié)果中，會對該問題進行描述，并對出現(xiàn)該問題的位置進行提示，從而幫助測試人員快速定位并對問題進行確認。

3 實驗

3.1 實驗數(shù)據(jù)

為了驗證SimREG工具的有效性，本文使用了兩套數(shù)據(jù)集，如表4所示。

a）FLIGHTCONROL。使用某飛行控制軟件的Simulink模型，針對本實驗中涉及的準則進行了問題注入，作為一個實驗數(shù)據(jù)集，該測試模型包含900多個模塊。本文重點針對本實驗中涉及的準則進行了問題注入，最終構(gòu)建的模型包含各類問題154個，其中有81個問題違反本實驗涉及的準則。問題分布如附錄所示。

b）CRITERION_Pamp;N。參照代碼檢查的模式［35］，使用前期設計Simulink建模準則時的正反例模型數(shù)據(jù)集進行實驗。該數(shù)據(jù)集包含1 300多個模塊，涉及各類問題共205個。本文并將其上傳到GitHub進行開源，成為一個公開數(shù)據(jù)集（https：//github.com/WangR121/SimulinkPositiveAndNegativeModel）。問題分布如附錄1所示。

3.2 對比方法

本文使用了兩類模型規(guī)則檢查工具與SimREG工具進行對比：a）目前最常用的Simulink規(guī)則檢查工具Model Advisor；b）基于元模型的檢查方法。為了驗證本文構(gòu)建的元模型的有效性，從1.3節(jié)提到的元模型中選擇了兩個元模型實現(xiàn)了本文設計的算法，即SLDG［21］與Massif［22］，并加入了對比實驗。對比工具如下所示：

a）Model Advisor工具。MATLAB提供的檢查工具可以檢查選擇的模型或子系統(tǒng)的條件和配置設置，包括導致不準確或低效仿真的條件。

b）基于SLDG［21］元模型實現(xiàn)的工具。SLDG元模型捕獲Simulink模型中存在的各種類型的依賴關系，原文用于模型指定元素的影響域分析等方面，本文將其用于模型的規(guī)則檢查中。

c）基于Massif［22］元模型實現(xiàn)的工具。Massif元模型定義了Simulink模型和EMF［36］模型的轉(zhuǎn)換范式，在原文中用于將Simulink導入到Eclipse插件中，在這里本文將其用于模型的規(guī)則檢查中。

3.3 實驗設置

本實驗使用的MATLAB/Simulink版本為R2015b，規(guī)則檢查工具SimREG基于MATLAB語言開發(fā)，并集成到Simulink應用中。實驗中使用命令腳本調(diào)用Model Advisor工具，腳本通過檢查項ID執(zhí)行對應的規(guī)則檢查過程。其他兩個基于元模型的工具，通過編寫相應的測試腳本進行調(diào)用。實驗對四個工具規(guī)則檢查結(jié)果的漏報率（1 negative rate，F(xiàn)NR）、誤報率（1 positive rate，F(xiàn)PR）和執(zhí)行時間進行了對比。

其中，漏報率（FNR）和誤報率（FPR）的計算方式為

FNR=FNCP，F(xiàn)PR=FPCR（1）

其中：FN為未檢測出的問題總數(shù);CP為存在的問題總數(shù);FP為誤報的問題總數(shù);CR為報出的問題總數(shù)。在實驗中本文更加關注漏報率（FNR）的對比結(jié)果。

執(zhí)行時間T通過公式T=Tend-Tstart計算，Tstart為執(zhí)行開始時間，Tend為執(zhí)行結(jié)束時間。

3.4 實驗結(jié)果與分析

3.4.1 規(guī)則檢查結(jié)果對比實驗

本文進行了對比實驗，對四個工具的漏報率和誤報率進行了比較。實驗結(jié)果如表5、6所示。

針對漏報率和誤報率的實驗結(jié)果分析如下：

a）SimREG工具在大部分情況下能夠發(fā)現(xiàn)更多的模型問題，相比于其他工具，漏報率降低30%～40%，誤報率降低10%～30%。在只需要對模型配置參數(shù)進行判定時，由于可以精確提取對應的配置內(nèi)容，能夠取得較好的檢查結(jié)果，如規(guī)則F_004，誤報率和漏報率都為0%。當檢查過程需要對信號的屬性進行判定時，由于很難追蹤到信號的起始位置，導致漏報率和誤報率較高，如規(guī)則F_018等，漏報率達到30%左右，誤報率達到20%左右。對規(guī)則F_020的檢查，由于本文在規(guī)則檢查算法設計中忽略了無符號數(shù)與數(shù)值直接進行比較的情況，漏報率和誤報率較高，都超過了20%，而且對信號的值或類型沒有提供前向的追溯，所以對于需要對信號值或類型進行判斷的規(guī)則支持力度較弱。

b）Model Advisor工具往往會將Stateflow中隱藏的問題忽略掉，導致漏報率相對較高，達到15%～30%，而且對其他一些規(guī)則檢查的誤報率也超過了20%，例如在對規(guī)則F_007的檢查中，Model Advisor工具將浮點數(shù)與 0的比較操作作為違反規(guī)則項進行了報告，使誤報率超過了30%。

c）基于SLDG［21］元模型實現(xiàn)的工具中，由于SLDG元模型針對模型中依賴關系進行設計，主要用于模型切片及影響域分析等，對規(guī)則檢查過程需要的模型信息提取不夠充分，導致檢查結(jié)果較差，漏報率達到20%～40%，誤報率達到20%～30%。例如未設計模型模塊間信號線的元模型元素，無法提取到模型連線信息，導致規(guī)則F_013檢查漏報率達到了40%。

d）基于Massif［22］元模型實現(xiàn)的工具中，元模型元素相對比較豐富，但缺乏針對性設計，導致誤報率較高，達到了20%～30%。另外由于沒有Stateflow部分的元模型設計，導致無法實現(xiàn)完整的規(guī)則檢查過程，使檢查結(jié)果的漏報率也較高，達到20%～40%，如規(guī)則F_002需要對Stateflow模型中的條件分支信息進行判定，當前工具無法實現(xiàn)該分析過程，導致漏報率達到了40%。

3.4.2 時間性能對比實驗

為了分析Simulink模型規(guī)則檢查過程的執(zhí)行效率，本文開展了時間性能實驗。實驗中對不同規(guī)模模型分別使用SimREG、Model Advisor、基于SLDG元模型和基于Massif元模型的工具進行相同準則項的檢查。在此，模型規(guī)模使用模型中包含的模塊數(shù)量進行簡單的表示。本文將模型中模塊的數(shù)量從200個模塊開始，每次增加500個模塊，最終形成一個包含7 200個模塊的大型模型，模型規(guī)模每次增大時，都使用SimREG、Model Advisor和其他兩個基于元模型的工具執(zhí)行一次規(guī)則檢查，并記錄消耗的時間。通過執(zhí)行時間對比，來驗證SimREG工具是否具有較好的檢查效率。由于時間的限制，本文無法完成如此大規(guī)模的模型設計，所以本文通過對初始模型的復用來逐漸增大模型規(guī)模。本文選擇了三條有代表性的準則進行實驗，其中準則F_004需要對模型配置進行檢查，準則F_011需要對信號或變量的值進行判斷，準則F_020需要對信號或變量的類型進行判定，覆蓋了規(guī)則檢查的幾個主要方向。檢查過程消耗時間（單位：s）分別如圖10所示。

從圖10中可以看出，SimREG等基于元模型的工具在執(zhí)行規(guī)則F_004、F_011時，檢查效率明顯優(yōu)于Model Advisor，執(zhí)行規(guī)則F_020時也有一定的優(yōu)勢，實驗結(jié)果分析如下：

a）SimREG工具總體檢查效率相比于Model Advisor工具提高約20%～80%，相對于其他基于元模型的工具大約有10%～20%的提高。這是由于本文方法針對規(guī)則設計，使用元模型對模型關鍵信息進行準確抽取，大大降低了處理的復雜度，使用遍歷方式完成模型的規(guī)則檢查過程，使計算時間隨著模型規(guī)模的增大呈線性增長趨勢。

b）Model Advisor工具需要對模型編譯后的中間文件進行分析，這些文件可能包含了許多復雜的、無用的信息，降低了處理的效率，尤其是在進行除零檢測時，花費時間較多。

c）其他基于元模型的檢查工具由于實現(xiàn)原理與SimREG工具類似，所以實驗結(jié)果也比較接近。根據(jù)不同元模型映射建立過程的復雜程度，時間消耗上有一定的偏差。如SLDG［21］元模型需要對模型進行數(shù)據(jù)流、控制流等方面的分析，過程比較復雜，因而需要相對較多的時間進行處理。

4 結(jié)束語

本文針對Simulink建模過程提出了41條與代碼生成相關的建模準則，并基于所設計的元模型，對每一條建模準則設計了相應的檢查算法來實現(xiàn)模型的規(guī)則檢查。本文實現(xiàn)的規(guī)則檢查工具SimREG相對于Model Advisor，具有準確率高、檢查速度快等優(yōu)點。而且由于元模型針對準則設計，構(gòu)建Simulink模型的元模型映射時，能夠準確提取需要的模型信息，避免無用信息的處理，相比于另外兩個基于元模型實現(xiàn)的工具，在檢查結(jié)果的誤報率、漏報率和檢查效率方面具有更好的效果。

雖然采用SimREG所獲得規(guī)則檢查結(jié)果的誤報率和漏報率低于Model Advisor等其他工具，但仍然無法完全消除，而且對于涉及信號值或類型的準則支持力度較弱，需要對檢查算法作進一步的完善。此外，對模型中檢查出的問題作出修改時，需要對模型進行修改點的影響域分析來幫助驗證修改的正確性。后續(xù)工作中，將繼續(xù)對以上問題展開研究。

附錄

數(shù)據(jù)集問題分布情況如下：

參考文獻：

[1]趙毅，胡蕓，龔家瑜，等.國內(nèi)軟件質(zhì)量與軟件測試標準化研究［J］.標準科學，2021，4（4）：25-31.（Zhao Yi， Hu Yun， Gong Jiayyu， et al. Research on domestic standardization of software quality and software testing［J］.Standard Science，2021，4（4）：25-31.）

［2]陳立前，吳國福，姜加紅.航天嵌入式軟件靜態(tài)分析技術［J］.空間控制技術與應用，2021，47（2）：86-92.（Chen Liqian， Wu Guofu， Jiang Jiahong. Static analysis technique for aerospace embedded software［J］.Aerospace Control and Application，2021，47（2）：86-92.）

［3]宋元章，沈湘衡，李洪雨.利用并行神經(jīng)網(wǎng)絡進行航天軟件質(zhì)量評價［J］.哈爾濱工程大學學報，2020，41（4）：595-600.（Song Yuanzhang， Shen Xiangheng， Li Hongyu. Quality evaluation of aero-space software using parallel neural networks［J］.Journal of Harbin Engineering University，2020，41（4）：595-600.）

［4]Bagnara R， Barr M， Hill P M. BARR-C：2018 and MISRA C：2012：synergy between the two most widely used C coding standards［EB/OL］.（2020-03-15）.https：//arxiv.org/abs/2003.06893.

［5]Famfulik J， Richtar M， Rehak R， et al. Application of hardware relia-bility calculation procedures according to ISO 26262 standard［J］.Quality and Reliability Engineering International，2020，36（6）：1822-1836.

［6]Meyers S. Effective C+： 55 specific ways to improve your programs and designs［M］.New York：Pearson Education，2005.

［7]Patel P， Bhatt C， Talati D. Structural coverage analysis with DO-178B standards［C］//Proc of International Conference on Advanced Computing Networking and Informatics.Singapore：Springer，2019：397-407.

［8]趙瑞蓮.軟件測試方法研究［D］.北京：中國科學院大學，2001.（Zhao Ruilian. Research on software testing methods［D］.Beijing： University of Chinese Academy of Sciences，2001.）

［9]張濤，秦凱，王楠，等.面向航天領域的模型驅(qū)動軟件設計開發(fā)方法［J］.航天控制，2017，35（5）：74-79，97.（Zhang Tao， Qin Kai， Wang Nan， et al. Research on model-driven aerospace software develop-ment method［J］.Aerospace Control，2017，35（5）：74-79，97.）

［10]仵林博，陳小紅，彭艷紅，等.基于SysML的嵌入式軟件系統(tǒng)建模與驗證方法研究［J］.計算機工程，2019，45（1）：1-8.（Wu Linbo， Chen Xiaohong， Peng Yanhong， et al. Research on system modeling and verification method of embedded software based on SysML［J］.Computer Engineering，2019，45（1）：1-8.）

［11]Nguyen C H， Nguyen T B N， Lu T Y V， et al. Apply a fuzzy algorithm to control an active suspension in a quarter car by MATLAB’s Simulink［J］.Applied Mechanics and Materials，2020，902：23-32.

［12]Rutishauser D， Moore R， Prothro J， et al. High performance computing for precision landing and hazard avoidance and co-design approach［C］//Proc of IEEE Aerospace Conference.Piscataway，NJ：IEEE Press，2019：1-10.

［13]MathWorks.Airbus使用基于模型的設計為A380開發(fā)出燃油管理系統(tǒng)［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/company/user_stories/airbus-develops-fuel-management-system-for-the-a380-using-model-based-design.html.（MathWorks.Airbus uses model-based design to develop a fuel management system for the A380［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/company/user_stories/airbus-develops-fuel-management-system-for-the-a380-using-model-based-design.html.）

［14]MathWorks.戴姆勒為梅賽德斯奔馳卡車設計巡航控制器［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/company/user_stories/daimler-designs-cruise-controller-for-mercedes-benz-trucks.html.（MathWorks.Daimler designs cruise controller for Mercedes-Benz trucks［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/company/user_stories/daimler-designs-cruise-controller-for-mercedes-benz-trucks.html.）

［15]MathWorks.濰柴動力借助基于模型的設計實現(xiàn)高壓共軌柴油發(fā)動機ECU軟件自主開發(fā)［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/company/user_stories/weichai-power-develops-ecu-so-ftware-for-high-pressure-common-rail-diesel-engine-in-house.html.（Math Works. WEICHAI realizes independent development of ECU software for high-pressure common rail diesel engines with the help of model-based design［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/company/user_stories/weichai-power-develops-ecu-software-for-high-pre-ssure-common-rail-diesel-engine-in-house.html.）

［16]MathWorks.東風電動車輛股份有限公司使用基于模型的設計開發(fā)混合動力電動汽車的電池管理系統(tǒng)［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/company/user_stories/dongfeng-electric-vehicle-develops-battery-management-system-for-hybrid-electricv-ehicles-using-model-based-design.html.（MathWorks.Dongfeng Electric Vehicle Co.，Ltd.uses model-based design to develop a battery management system for hybrid electric vehicles［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/company/user_stories/dongfeng-electric-vehicle-develops-battery-management-system-for-hybrid-electric vehicles-using-model-based-design.html.）

［17]Kim Y G， Yoon H S. Research on the effects of MAAB style guidelines for weapon system embedded software reliability improvement［J］.Journal of the Korea Institute of Military Science and Technology，2014，17（2）：213-222.

［18]Pantelic V， Postma S， Lawford M， et al. Software engineering practices and Simulink：bridging the gap［J］.International Journal on Software Tools for Technology Transfer，2018，20（1）：95-117.

［19]MathWorks.MAB建模規(guī)范［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/help/simulink/mab-modeling-guidelines.html.（MathWorks.MAB modeling guidelines［EB/OL］.［2021-04-20］.https：//ww2.mathworks.cn/help/simulink/mab-modeling-guidelin-es.html.）

［20]中國人民解放軍總裝備部電子信息基礎部.GJB 8114—2013，中華人民共和國國家軍用標準C/C+語言編程安全子集［S］.北京：總裝備部軍標出版發(fā)行部，2013.（Electronic Information Basic Department of General Armament Department of Chinese People’s Liberation Army.GJB 8114—2013，Standard C/C+ language programming security subset of the People’s Republic of China National Military［S］.Beijing：Military Standard Publication and Distribution Department of General Armament Department，2013.）

［21]Prasad S， Nayak S， Vijay V， et al. SLDG： a metamodel for Simulink/Stateflow models and its applications［J］.Innovations in Systems and Software Engineering，2016，12（4）：263-278.

［22]Sánchez B， Zolotas A， Hoyos Rodriguez H， et al. On-the-fly translation and execution of OCL-like queries on Simulink models［C］//Proc of the 22nd International Conference on Model Driven Engineering Languages and Systems.Piscataway，NJ：IEEE Press，2019：205-215.

［23]郭丹青，呂繼東，王淑靈，等.中國高速鐵路列控系統(tǒng)的形式化分析與驗證［J］.中國科學：信息科學，2015，45（3）：417-438.（Guo Danqing， Lyu Jidong， Wang Shuling， et al. Formal analysis and verification of Chinese train control system［J］.Scientia Sinica：Informationis，2015，45（3）：417-438.）

［24]Novikov A S， Ivutin A N， Troshina A G， et al. The approach to fin-ding errors in program code based on static analysis methodology［C］//Proc of the 6th Mediterranean Conference on Embedded Com-" "puting.Piscataway，NJ：IEEE Press，2017：1-4.

［25]Jang J， Kang Y， Lee J. Static analysis and improvement opportunities for open source of UAV flight control software［J］.Journal of the Korean Society for Aeronautical amp; Space Sciences，2021，49（6）：473-480.

［26]Gautam S. Comparison of Java programming testing tools［J］.International Journal of Engineering Technologies and Management Research，2018，5（2）：66-76.

［27]周培.基于LDRA Testbed的民用機載軟件靜態(tài)測試方法［J］.計算機測量與控制，2019，27（7）：107-110，149.（Zhou Pei. Civil airborne software static testing method based on LDRA Testbed［J］.Computer Measurement amp; Control，2019，27（7）：107-110，149.）

［28]李鋒.航天C程序安全規(guī)則檢查技術研究［D］.北京：國防科學技術大學，2010.（Li Feng. Research on inspection technology of aerospace C program safety rules［D］.Beijing：National University of Defense Technology，2010.）

［29]MathWorks.使用模型顧問檢查您的模型［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/help/simulink/ug/select-and-run-model-advisor-checks.html.（MathWorks. Check your model using the model advisor［EB/OL］.［2021-04-06］.https：//ww2.mathworks.cn/help/simulink/ug/select-and-run-model-advisor-checks.html.）

［30]Ma Zhiyi， He Huihong， Liu Jinyang， et al. Analysis of the evolution of the UML metamodel［C］//Proc of the 6th International Conference on Model-Driven Engineering and Software Development.2018：356-363.

［31]Maschotta R， Wichmann A， Zimmermann A， et al. Integrated automotive requirements engineering with a SysML-based domain-specific language［C］//Proc of IEEE International Conference on Mechatro-nics.Piscataway，NJ：IEEE Press，2019：402-409.

［32]Su Bing， Dong Yancen， Wu Ji. Generation of Simulink simulation model script based on architecture model［C］//Proc of the 2nd International Conference on Computer Science and Network Technology.Piscataway，NJ：IEEE Press，2012：1340-1344.

［33]Legros E， Schfer W， Schürr A， et al. 14 MATE-a model analysis and transformation environment for MATLAB Simulink［C］//Proc of Dagstuhl Workshop on Model-Based Engineering of Embedded Real-Time Systems.Berlin：Springer，2007：323-328.

［34]Son H S， Kim W Y， Kim R Y， et al. Metamodel design for model transformation from Simulink to ECML in cyber physical systems［M］//Kim T， Cho H， Gervasi O， et al. Computer Applications for Gra-phics， Grid Computing， and Industrial Environment.Berlin：Springer，2012：56-60.

［35]Shi Qingkai， Wu Rongxin， Fan Gang， et al. Conquering the extensional scalability problem for value-flow analysis frameworks［C］//Proc of the 42nd International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2020：812-823.

［36]Eclipse Foundation. Eclipse modeling framework（EMF）［EB/OL］.［2021-07-04］.http：//www.eclipse.org/modeling/emf/.