01

引 言

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

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

SmartRocket Modeler

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

02

研發(fā)背景

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

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

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

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

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

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

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

03

理論支撐

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

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

? 手動編碼與用戶需求難以完全貼合；

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

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

? ......

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

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

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

? 簡化軟件開發(fā)過程，縮短軟件開發(fā)周期與成本；

? ......

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

2. 同步假設(shè)

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

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

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

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

? 運行周期之間不會重疊。

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

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

SmartRocket Modeler功能背后以Lustre語言為支撐，提供具有精確語義的可驗證模型的構(gòu)建、驗證、測試和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)境變量；

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

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

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

04

產(chǎn)品功能

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

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

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

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

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

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

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

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

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

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

05

總 結(jié)

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

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

審核編輯 黃宇