01

引 言

在航空航天、軌道交通、核能電力、汽車(chē)電子等安全關(guān)鍵領(lǐng)域，嵌入式控制軟件一旦出現(xiàn)故障，其造成的損失無(wú)法接受。面對(duì)軟件規(guī)模和復(fù)雜度的不斷提升，傳統(tǒng)的軟件開(kāi)發(fā)方法已無(wú)法滿足越來(lái)越繁雜龐大的安全關(guān)鍵系統(tǒng)。為應(yīng)對(duì)這一挑戰(zhàn)，上?？匕惭邪l(fā)了高可信嵌入式軟件建模開(kāi)發(fā)工具SmartRocket Modeler。

高可信嵌入式軟件建模開(kāi)發(fā)工具

SmartRocket Modeler

本文主要介紹SmartRocket Modeler工具的研發(fā)背景、核心理論支撐、功能模塊概覽，闡述它如何為復(fù)雜軟件的開(kāi)發(fā)提供更可靠、高效的解決方案。

02

研發(fā)背景

嵌入式控制軟件是嵌入式系統(tǒng)的重要組成部分，在航空航天、軌道交通、核能電力、汽車(chē)電子等安全攸關(guān)領(lǐng)域的重要性尤為突出，一旦出現(xiàn)故障，其造成的損失無(wú)法接受。如波音737 Max墜機(jī)事件是由自動(dòng)失速防止系統(tǒng)（MCAS）的軟件缺陷導(dǎo)致的未能準(zhǔn)確處理傳感器故障造成的，最終導(dǎo)致346人遇難，經(jīng)濟(jì)損失達(dá)4萬(wàn)億元的嚴(yán)重后果。

隨著計(jì)算機(jī)技術(shù)的快速發(fā)展、工業(yè)制造業(yè)的不斷升級(jí)，對(duì)安全關(guān)鍵系統(tǒng)的要求也越來(lái)越嚴(yán)格，從而使得軟件應(yīng)用在安全關(guān)鍵系統(tǒng)中承擔(dān)越來(lái)越多的功能。與此同時(shí)軟件的規(guī)模和復(fù)雜度也不斷提升，導(dǎo)致軟件的缺陷密度和失效問(wèn)題也顯著增加。采用傳統(tǒng)的軟件開(kāi)發(fā)方法來(lái)進(jìn)行現(xiàn)代高可信嵌入式軟件開(kāi)發(fā)具有研發(fā)工作反復(fù)進(jìn)行、研發(fā)周期大幅延長(zhǎng)、成本大幅度增加、軟件難以進(jìn)行維護(hù)以及升級(jí)等問(wèn)題。近半個(gè)世紀(jì)以來(lái)，由于軟件問(wèn)題造成安全關(guān)鍵系統(tǒng)出現(xiàn)故障所導(dǎo)致的損失難以衡量，傳統(tǒng)的軟件開(kāi)發(fā)模式已無(wú)法滿足越來(lái)越繁雜龐大的安全關(guān)鍵系統(tǒng)。因此SmartRocket Modeler可視化建模開(kāi)發(fā)工具應(yīng)需而生。它可以根據(jù)用戶在可視化建模系統(tǒng)中所建立的應(yīng)用軟件模型，自動(dòng)生成應(yīng)用軟件的框架和源代碼。其優(yōu)點(diǎn)包括：

? 構(gòu)建的模型不具有二義性，可讀性強(qiáng)。在代碼自動(dòng)生成的過(guò)程中，可以通過(guò)可視化圖形界面的方式讓用戶使用起來(lái)更加明確、清晰，唯一模型便于交流和維護(hù)；

? 代碼自動(dòng)生成具有特定規(guī)則。通過(guò)加載預(yù)先定制好的模型庫(kù)，自動(dòng)生成代碼的規(guī)范性可以大幅度提升；

? 準(zhǔn)確且高效。模型在進(jìn)行代碼生成前需經(jīng)過(guò)驗(yàn)證，保證正確的模型生成正確的代碼。避免手工編程帶來(lái)的繁瑣和與需求不一致性的風(fēng)險(xiǎn)，從而保證代碼質(zhì)量符合規(guī)則要求；

? 在縮短軟件開(kāi)發(fā)周期的情況下，可節(jié)省時(shí)間、節(jié)約成本、大大減少代碼錯(cuò)誤產(chǎn)生率。

該產(chǎn)品可實(shí)現(xiàn)國(guó)外壟斷工具SCADE Suite的國(guó)產(chǎn)化替代，解決需求建模、驗(yàn)證領(lǐng)域的“卡脖子”技術(shù)，可填補(bǔ)國(guó)內(nèi)在數(shù)據(jù)流可視化建模和驗(yàn)證領(lǐng)域的空白，并達(dá)到國(guó)內(nèi)先進(jìn)水平。

03

理論支撐

1. 從V字開(kāi)發(fā)模型到Y(jié)字開(kāi)發(fā)模型

傳統(tǒng)的“V”字軟件開(kāi)發(fā)流程中，以文檔開(kāi)發(fā)為中心，用戶經(jīng)歷需求分析-概要設(shè)計(jì)-詳細(xì)設(shè)計(jì)-編碼-單元測(cè)試-集成測(cè)試-系統(tǒng)測(cè)試等階段，得到相對(duì)可靠的軟件產(chǎn)品。在此過(guò)程中，由于自然語(yǔ)言的二義性、文檔溝通難以完全表述清晰等原因，可能存在如下問(wèn)題：

? 手動(dòng)編碼與用戶需求難以完全貼合；

? 以代碼為核心，早期開(kāi)發(fā)難以驗(yàn)證；

? 安全關(guān)鍵領(lǐng)域要求高，編碼邏輯易混亂。

? ......

而符合MBSE的“Y”字開(kāi)發(fā)則具有如下優(yōu)勢(shì)：

? 人機(jī)互動(dòng)友好易用，模塊化設(shè)計(jì)，便于資產(chǎn)留存和理解；

? 以模型為中心，避免實(shí)現(xiàn)過(guò)程二義性；

? 簡(jiǎn)化軟件開(kāi)發(fā)過(guò)程，縮短軟件開(kāi)發(fā)周期與成本；

? ......

因此，對(duì)于功能安全性和可靠性要求更高的嵌入式控制軟件，更適合使用SmartRocket Modeler提供的基于模型的開(kāi)發(fā)方式。

2. 同步假設(shè)

同步假設(shè)是指假設(shè)反應(yīng)式系統(tǒng)響應(yīng)速度足夠快，則系統(tǒng)接收環(huán)境輸入后可立即響應(yīng)并產(chǎn)生輸出，并等待下一個(gè)輸入，在此期間系統(tǒng)內(nèi)部狀態(tài)保持不變。對(duì)于嵌入式控制系統(tǒng)而言，系統(tǒng)周期性運(yùn)行，一個(gè)周期內(nèi)的計(jì)算瞬時(shí)完成，不會(huì)存在系統(tǒng)資源不足或超時(shí)的情況。

在實(shí)際運(yùn)行中，由于技術(shù)或成本的限制，一般是通過(guò)控制系統(tǒng)獲得任意兩次輸入的時(shí)間間隔大于系統(tǒng)的響應(yīng)時(shí)間的方式來(lái)實(shí)現(xiàn)同步假設(shè)的。當(dāng)周期性運(yùn)行的系統(tǒng)滿足如下條件時(shí)，即可認(rèn)為符合同步假設(shè)：

? 系統(tǒng)在周期開(kāi)始時(shí)獲得輸入，且當(dāng)前周期內(nèi)輸入不變；

? 中間變量與輸出變量在周期內(nèi)計(jì)算后，值在本周期內(nèi)不會(huì)改變；

? 運(yùn)行周期之間不會(huì)重疊。

3. 同步數(shù)據(jù)流語(yǔ)言Lustre

Lustre建模語(yǔ)言每一個(gè)變量都代表一個(gè)數(shù)據(jù)流，流是一個(gè)給定數(shù)據(jù)類(lèi)型的值的無(wú)限序列，具有數(shù)值和時(shí)鐘兩個(gè)特性。Lustre提供的時(shí)間運(yùn)算符對(duì)數(shù)據(jù)流進(jìn)行采樣，也可以獲取之前周期的流值，為控制系統(tǒng)的建模提供了方便。其主要應(yīng)用領(lǐng)域有自動(dòng)化控制以及信號(hào)處理系統(tǒng)等。

SmartRocket Modeler功能背后以Lustre語(yǔ)言為支撐，提供具有精確語(yǔ)義的可驗(yàn)證模型的構(gòu)建、驗(yàn)證、測(cè)試和C代碼生成等功能。

4. 反應(yīng)式系統(tǒng)

SmartRocket Modeler面向反應(yīng)式系統(tǒng)，即與環(huán)境持續(xù)交互的系統(tǒng)。反應(yīng)式系統(tǒng)可看作序列到序列的函數(shù)，其工作模式為：

? 反應(yīng)式系統(tǒng)讀入環(huán)境變量；

? 計(jì)算出邏輯運(yùn)算結(jié)果，并反饋至環(huán)境中；

? 通過(guò)系統(tǒng)邏輯運(yùn)算更改內(nèi)部狀態(tài)。

當(dāng)使用f作為反應(yīng)式系統(tǒng)的一次邏輯計(jì)算時(shí)，工作模式可以表達(dá)為：

04

產(chǎn)品功能

SmartRocket Modeler工具面向航空航天、軌道交通、核能、汽車(chē)電子等領(lǐng)域，作用于傳統(tǒng)軟件開(kāi)發(fā)流程的詳細(xì)設(shè)計(jì)階段和編碼階段，提供模型設(shè)計(jì)、分析、測(cè)試、代碼生成一系列功能。

1. 圖形化建模：根據(jù)對(duì)系統(tǒng)需求的分析，運(yùn)用數(shù)據(jù)流構(gòu)件、狀態(tài)機(jī)構(gòu)件庫(kù)進(jìn)行基于模型的系統(tǒng)設(shè)計(jì)。圖形化建?；谕綌?shù)據(jù)流語(yǔ)言，因此建模機(jī)制具有嚴(yán)格的數(shù)學(xué)語(yǔ)義。Modeler提供的構(gòu)件庫(kù)包含數(shù)學(xué)構(gòu)件、比較構(gòu)件、數(shù)組/結(jié)構(gòu)體構(gòu)件、邏輯構(gòu)件、位構(gòu)件、時(shí)態(tài)構(gòu)件、分支構(gòu)件、條件塊構(gòu)件、狀態(tài)機(jī)構(gòu)件和高階構(gòu)件等，支持?jǐn)?shù)據(jù)流和狀態(tài)機(jī)建模，全面對(duì)標(biāo)SCADE Suite建模算子。

2. 靜態(tài)分析：靜態(tài)分析通過(guò)從設(shè)計(jì)模型中抽取出的多層次模型刻面，充分呈現(xiàn)系統(tǒng)不同層次的功能、行為、數(shù)據(jù)定義及數(shù)據(jù)傳遞特征，用于進(jìn)行交互式完整性檢查。檢查模型是否滿足預(yù)定義的設(shè)計(jì)規(guī)則的維度包含類(lèi)型檢查、數(shù)據(jù)依賴關(guān)系分析、狀態(tài)遷移分析?？蓭椭O(shè)計(jì)人員在開(kāi)發(fā)的早期就排除模型中的基本錯(cuò)誤。

3. 耦合度分析：耦合度分析功能以報(bào)告的形式展示項(xiàng)目模型中控制耦合（CC）、數(shù)據(jù)耦合（DC）的分析結(jié)果。工具提供的耦合度分析功能可幫助航空航天領(lǐng)域的客戶滿足DO-178B/C相關(guān)規(guī)定。

4. 模擬仿真：模擬仿真功能通過(guò)模型仿真和斷點(diǎn)調(diào)試確保模型在特定物理場(chǎng)景中的動(dòng)態(tài)運(yùn)行能力，并對(duì)運(yùn)行結(jié)果進(jìn)行可視化展示滿足更直觀的分析。該功能包含兩種模式：基于模型的仿真調(diào)試和基于C代碼的仿真調(diào)試。 對(duì)于同樣的仿真用例，兩種仿真模式的仿真結(jié)果相同。

5. 基于模型的測(cè)試：工具提供基于模型的測(cè)試功能。分為批量測(cè)試和覆蓋率分析兩個(gè)部分。批量測(cè)試功能允許用戶同時(shí)執(zhí)行多個(gè)測(cè)試用例文件，驗(yàn)證模型運(yùn)行結(jié)果是否符合預(yù)期，確保設(shè)計(jì)模型的正確性。覆蓋率分析功能基于測(cè)試用例文件進(jìn)行指定覆蓋準(zhǔn)則的覆蓋率分析，可選擇的覆蓋率準(zhǔn)則包括：OMC/DC、influence、ODC。

6. 代碼生成：在排除模型早期錯(cuò)誤，保障模型一致性、正確性和安全性基礎(chǔ)上，通過(guò)模型、LUSTRE 語(yǔ)言、代碼轉(zhuǎn)換，工具可實(shí)現(xiàn) C 代碼自動(dòng)生成，有效減少用戶重復(fù)編碼工作。

7. 代碼與模型的追溯：工具提供模型與代碼的追溯查看，以變量為單位，直觀展示C 代碼和模型的對(duì)應(yīng)關(guān)系，從側(cè)面證明代碼生成的可靠性。

8. 設(shè)計(jì)文檔生成：工具支持對(duì)模型的設(shè)計(jì)文檔自動(dòng)生成，封面信息可進(jìn)行配置，提供生成格式為html和docx文檔。

9. 模型遷移：Modeler對(duì)SCADE Suite的模型進(jìn)行了兼容，支持現(xiàn)有SCADE項(xiàng)目的一鍵導(dǎo)入，以及Modeler項(xiàng)目的一鍵導(dǎo)出，無(wú)縫銜接現(xiàn)有開(kāi)發(fā)流程，便于模型資產(chǎn)復(fù)用。

05

總 結(jié)

SmartRocket Modeler基于嚴(yán)謹(jǐn)?shù)睦碚摵凸こ虒?shí)踐，為高可信嵌入式軟件的開(kāi)發(fā)提供了從建模、驗(yàn)證到代碼生成的全流程支持。

本文主要介紹了工具的起源與核心理論。在后續(xù)的推送中，我們將逐一詳細(xì)介紹各項(xiàng)具體功能，如圖形化建模、靜態(tài)分析、代碼生成等，歡迎您持續(xù)關(guān)注。

審核編輯 黃宇