01

引 言

在上一篇推送中（面向復雜系統(tǒng)的嵌入式軟件高可信建模與驗證方法），我們介紹了上?？匕惭邪l(fā)的高可信嵌入式軟件建模開發(fā)工具SmartRocket Modeler。它基于嚴謹?shù)耐綌?shù)據(jù)流語言理論，為航空航天、軌道交通等安全關鍵領域的嵌入式軟件開發(fā)，提供了從建模、驗證到代碼生成的全流程支持。本文將深入探討SmartRocket Modeler的核心功能之一——圖形化建模，詳細闡述它如何將復雜、抽象的系統(tǒng)需求，轉化為直觀、精確、無二義性的可視化模型，從而為構建高可靠性的嵌入式軟件奠定堅實的基礎。

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

SmartRocket Modeler

02

為何需要圖形化建模？

傳統(tǒng)的軟件開發(fā)方法，在需求分析、詳細設計和編碼階段，主要依賴自然語言描述的文檔和手寫代碼。這種方式存在著天然的鴻溝：自然語言固有的二義性，使得需求分析人員、設計人員與編碼人員之間對同一功能的理解容易出現(xiàn)偏差；隨著軟件規(guī)模的增長，用文字難以清晰描述系統(tǒng)中錯綜復雜的數(shù)據(jù)流和控制邏輯，設計缺陷難以在早期發(fā)現(xiàn)；手動編碼不僅效率低下，而且容易引入與設計不符的人為錯誤，對安全關鍵系統(tǒng)而言，這種風險是致命的。

為了解決這些問題，基于模型的設計方法應運而生。SmartRocket Modeler的圖形化建模功能，正是這一方法論的最佳實踐。它允許工程師使用標準化的圖形元素（如數(shù)據(jù)流圖、狀態(tài)機）來構建系統(tǒng)。這個模型不僅是設計的藍圖，更是后續(xù)仿真、驗證和代碼自動生成的唯一、精確的源頭，從根本上解決了傳統(tǒng)開發(fā)模式的痛點。

03

核心理論與技術支撐

1. 從“以文檔為中心”到“以模型為中心”

回顧第一篇中提到的軟件開發(fā)“V字模型”，其核心是“以文檔為中心”。而SmartRocket Modeler所倡導的，是基于模型的“Y字開發(fā)流程”。圖形化建模正是實現(xiàn)這一轉變的關鍵。

在“Y字模型”中，圖形化模型取代了冗長的設計文檔，成為開發(fā)流程的核心資產(chǎn)。所有的后續(xù)工作，如分析、仿真、測試和代碼生成，都圍繞這個統(tǒng)一的模型展開。這種轉變帶來的優(yōu)勢是革命性的：

? 消除二義性：模型具有精確的數(shù)學語義，確保了設計與實現(xiàn)的高度一致性。

? 早期驗證：在設計階段即可對模型進行仿真運行，直觀地驗證功能邏輯是否符合預期，將缺陷消滅在萌芽狀態(tài)。

? 高效溝通：圖形化的表達方式直觀易懂，能夠有效拉近領域專家、系統(tǒng)工程師和軟件開發(fā)人員之間的距離，降低溝通成本。

? 自動化實現(xiàn)：基于模型可以自動生成高質量的生產(chǎn)級代碼，將工程師從繁瑣易錯的手工編碼中解放出來。

2. 堅實的理論基石：同步數(shù)據(jù)流與Lustre語言

SmartRocket Modeler圖形化建模的強大功能，并非空中樓閣，而是建立在同步假設和同步數(shù)據(jù)流語言Lustre這兩個堅實的理論基礎之上。同步假設是反應式系統(tǒng)建模的核心。它假設系統(tǒng)在接收輸入的瞬間就能完成計算并產(chǎn)生輸出，然后等待下一個時鐘周期。這為復雜的嵌入式控制邏輯提供了簡潔而強大的時間抽象，使得工程師可以專注于功能邏輯的設計，而無需過早陷入復雜的時間調度細節(jié)。而同步數(shù)據(jù)流語言Lustre則是SmartRocket Modeler的“靈魂”。每個圖形化構件、每一條數(shù)據(jù)連線，在后臺都對應著精確的Lustre代碼。Lustre語言將系統(tǒng)中的所有變量都視為隨時間變化的“數(shù)據(jù)流”，并提供了豐富的操作符（如算術運算、邏輯運算、以及`pre`（前一周期值）、`->`（初始化）等時態(tài)算子）來對這些流進行操作。這種嚴格的數(shù)學語義保證了模型的確定性、完整性和一致性，為后續(xù)的形式化驗證和高質量代碼生成提供了可能。

因此，您在SmartRocket Modeler畫布上拖拽的每一個構件，連接的每一條線，都是在“書寫”一份形式化的、可驗證的、無二義性的系統(tǒng)規(guī)范。

04

產(chǎn)品功能：圖形化建模

SmartRocket Modeler的圖形化建模環(huán)境，旨在為用戶提供高效、直觀、所見即所得的設計體驗。它不僅僅是將構件簡單羅列，而是提供了一套完整、強大的建模體系。

1. 豐富的建模元素庫

工欲善其事，必先利其器。SmartRocket Modeler提供了涵蓋11個大類、超過66個精心設計的圖形化構件，全面對標國際主流工具SCADE Suite的建模算子，能夠滿足各種復雜嵌入式系統(tǒng)的建模需求。

? 基礎運算構件：包括數(shù)學構件（加、減、乘、除等）、比較構件（大于、小于、等于等）、邏輯構件（與、或、非等）和位構件（移位、按位與/或等），用于構建核心的算法邏輯。

? 數(shù)組/結構體構件：專門為處理復雜數(shù)據(jù)結構設計，如針對數(shù)組的`Concatenation`（拼接）、`Reverse`（反轉）、`Transpose`（轉置）構件，針對結構體的`Make`（構建）、`Flatten`（展開）構件，方便用戶高效地操作和管理數(shù)據(jù)。

?時態(tài)構件：如`Pre`（取前一周期值）、`Init`（初始化）、`FollowedBy`（延遲N個周期），是構建具有“記憶”功能的時序邏輯的基礎。

? 狀態(tài)機構件：提供完整的狀態(tài)機建模支持，包括狀態(tài)(State)、遷移(Transition)，并支持強遷移、弱遷移、同步遷移等多種遷移語義，以及Restart/Resume等高級屬性，完美描述系統(tǒng)的控制流和模式切換。

? 高階構件：通過高階構件（如Map、Fold、MapFold等迭代器）和激活構件（如Boolean Activate），允許用戶在更高的抽象層次上建模，實現(xiàn)復雜的循環(huán)、迭代和條件執(zhí)行邏輯，極大地提升了建模的簡潔性和表達力。

2. 靈活的建模方式

SmartRocket Modeler充分考慮了不同用戶的使用習慣和復雜場景下的設計需求，提供了多種靈活的設計方式：

? 自頂向下與自底向上設計：支持從系統(tǒng)頂層開始，逐步細化分解功能模塊；也支持先構建底層的基礎組件，再通過組合搭建完整的系統(tǒng)。

? 圖形與文本的無縫融合：

- 圖形畫布：是主要的建模場所，用戶通過拖拽構件、繪制連線，可以直觀地構建數(shù)據(jù)流圖和狀態(tài)機。

- 文本畫布：支持在組件內部直接編寫Lustre文本代碼，為熟悉文本方式的用戶或處理某些復雜的表達式提供了便利。圖形畫布可以一鍵轉換為文本畫布。

? 多畫布設計：對于一個復雜的組件，允許創(chuàng)建多個圖形/文本畫布，通過中間變量進行邏輯連接。其作用是將復雜的模型分解為多個邏輯清晰的步驟，極大地提升了大型模型的可讀性和可維護性。

3. 強大的模型管理能力

? 類型系統(tǒng)：提供強類型的建模環(huán)境，支持基本類型（int8、uint32、float64、bool等）以及用戶自定義的數(shù)組(Array)、結構體(Structure)、枚舉(Enum) 和基礎類型別名，確保模型在數(shù)據(jù)層面上的精確性。

? 構件庫與資產(chǎn)復用：

- 內置類庫：工具自帶多個系統(tǒng)類庫，提供了常用的預定義組件。

- 用戶類庫：用戶可以將自己開發(fā)的、經(jīng)過驗證的模塊作為私有類庫在多個項目中輕松復用，實現(xiàn)知識和資產(chǎn)的沉淀。

? SCADE模型遷移：支持一鍵導入SCADE Suite的模型文件（.etp格式），并能將Modeler項目導出為SCADE兼容格式，實現(xiàn)了與現(xiàn)有開發(fā)生態(tài)的無縫銜接，有效保護歷史資產(chǎn)。

05

總 結

圖形化建模是SmartRocket Modeler的核心價值所在。它不僅僅是一個畫圖工具，更是一個基于嚴格形式化語義的設計與思考平臺。通過提供豐富而精確的建模元素、靈活的設計方式以及強大的模型管理能力，SmartRocket Modeler幫助工程師將錯綜復雜的嵌入式軟件需求，轉化為清晰、無二義性、可驗證、可執(zhí)行的模型。

這標志著軟件開發(fā)的重心，從難以捉摸的文檔和易錯的手工編碼，轉移到了精確、直觀的模型之上。它為后續(xù)的靜態(tài)分析、模擬仿真、形式化驗證和自動化代碼生成奠定了堅實的基礎，是打造高可信、高安全嵌入式控制軟件的不二之選。

在接下來的推送中，我們將繼續(xù)深入探索SmartRocket Modeler的其他關鍵功能，如靜態(tài)分析與驗證，敬請期待。

審核編輯 黃宇