01

引 言

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

高可信嵌入式軟件建模開發工具

SmartRocket Modeler

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

02

研發背景

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

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

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

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

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

? 在縮短軟件開發周期的情況下，可節省時間、節約成本、大大減少代碼錯誤產生率。

該產品可實現國外壟斷工具SCADE Suite的國產化替代，解決需求建模、驗證領域的“卡脖子”技術，可填補國內在數據流可視化建模和驗證領域的空白，并達到國內先進水平。

03

理論支撐

1. 從V字開發模型到Y字開發模型

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

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

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

? 安全關鍵領域要求高，編碼邏輯易混亂。

? ......

而符合MBSE的“Y”字開發則具有如下優勢：

? 人機互動友好易用，模塊化設計，便于資產留存和理解；

? 以模型為中心，避免實現過程二義性；

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

? ......

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

2. 同步假設

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

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

? 系統在周期開始時獲得輸入，且當前周期內輸入不變；

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

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

3. 同步數據流語言Lustre

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

SmartRocket Modeler功能背后以Lustre語言為支撐，提供具有精確語義的可驗證模型的構建、驗證、測試和C代碼生成等功能。

4. 反應式系統

SmartRocket Modeler面向反應式系統，即與環境持續交互的系統。反應式系統可看作序列到序列的函數，其工作模式為：

? 反應式系統讀入環境變量；

? 計算出邏輯運算結果，并反饋至環境中；

? 通過系統邏輯運算更改內部狀態。

當使用f作為反應式系統的一次邏輯計算時，工作模式可以表達為：

04

產品功能

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

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

2. 靜態分析：靜態分析通過從設計模型中抽取出的多層次模型刻面，充分呈現系統不同層次的功能、行為、數據定義及數據傳遞特征，用于進行交互式完整性檢查。檢查模型是否滿足預定義的設計規則的維度包含類型檢查、數據依賴關系分析、狀態遷移分析。可幫助設計人員在開發的早期就排除模型中的基本錯誤。

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

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

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

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

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

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

9. 模型遷移：Modeler對SCADE Suite的模型進行了兼容，支持現有SCADE項目的一鍵導入，以及Modeler項目的一鍵導出，無縫銜接現有開發流程，便于模型資產復用。

05

總 結

SmartRocket Modeler基于嚴謹的理論和工程實踐，為高可信嵌入式軟件的開發提供了從建模、驗證到代碼生成的全流程支持。

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

審核編輯 黃宇