01

引 言

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

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

SmartRocket Modeler

02

為何需要圖形化建模？

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

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

03

核心理論與技術(shù)支撐

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

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

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

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

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

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

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

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

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

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

04

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

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

1. 豐富的建模元素庫

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

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

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

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

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

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

2. 靈活的建模方式

SmartRocket Modeler充分考慮了不同用戶的使用習(xí)慣和復(fù)雜場景下的設(shè)計(jì)需求，提供了多種靈活的設(shè)計(jì)方式：

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

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

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

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

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

3. 強(qiáng)大的模型管理能力

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

? 構(gòu)件庫與資產(chǎn)復(fù)用：

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

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

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

05

總 結(jié)

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

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

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

審核編輯 黃宇