行業(yè)背景

隨著計算機技術(shù)的快速發(fā)展、工業(yè)制造業(yè)的不斷升級，對安全關(guān)鍵系統(tǒng)的要求也越來越嚴格，從而使得軟件應用在安全關(guān)鍵系統(tǒng)中承擔越來越多的功能。與此同時軟件的規(guī)模和復雜度也不斷提升，導致軟件的缺陷密度和失效問題也顯著增加。近半個世紀以來，由于軟件問題造成安全關(guān)鍵系統(tǒng)出現(xiàn)故障所導致的損失難以衡量，傳統(tǒng)的軟件開發(fā)模式已無法滿足越來越繁雜龐大的安全關(guān)鍵系統(tǒng)，因此SmartRocket Modeler可視化建模開發(fā)工具應需而生。該產(chǎn)品可實現(xiàn)國外壟斷工具的國產(chǎn)化替代，解決需求建模、驗證領(lǐng)域的“卡脖子”技術(shù)，可填補國內(nèi)在數(shù)據(jù)流可視化建模和驗證領(lǐng)域的空白，并達到國內(nèi)先進水平。

產(chǎn)品概述

SmartRocket Modeler是一款國產(chǎn)自主可控的可視化建模開發(fā)工具。該工具支持嵌入式軟件模型的設(shè)計與開發(fā)，能夠從系統(tǒng)需求出發(fā)，為用戶提供基于Lustre模型語言的圖形化建模、模型靜態(tài)檢查、模型仿真與調(diào)試、模型在環(huán)測試、C代碼自動生成等豐富便捷的功能。同時工具也支持全系列國產(chǎn)操作系統(tǒng)，為國內(nèi)高端制造領(lǐng)域的嵌入式軟件研制提供支撐平臺，為逐步擺脫對國外同類軟件的依賴提供有效解決方案。

產(chǎn)品功能

01圖形化建模

根據(jù)對系統(tǒng)需求的分析，運用數(shù)據(jù)流構(gòu)件、狀態(tài)機構(gòu)件庫進行基于模型的系統(tǒng)設(shè)計。建模機制具有嚴格的數(shù)學語義。

02模型靜態(tài)檢查

從設(shè)計模型的類型檢查、量綱檢查、數(shù)據(jù)依賴關(guān)系分析、狀態(tài)遷移分析四個維度分析模型是否滿足預定義的設(shè)計規(guī)則。

03模型仿真與調(diào)試

通過模型仿真和斷點調(diào)試確保模型在特定物理場景中動態(tài)運行能力，并對運行結(jié)果進行可視化展示滿足更直觀的分析。

04運行時驗證

對需要驗證性質(zhì)進行性質(zhì)關(guān)聯(lián)并驗證構(gòu)建的性質(zhì)模型，確保是否滿足待驗性質(zhì)從而來保證模型的安全性與可靠性。

05代碼自動生成

在排除模型早期錯誤，保障模型一致性、正確性和安全性基礎(chǔ)上，通過模型、LUSTRE語言、代碼轉(zhuǎn)換，實現(xiàn)C代碼自動生成。

06報告生成與定制

針對模型靜態(tài)檢查、仿真與調(diào)試、運行時驗證等過程，生成相應報告供用戶查看與存檔，同時測試報告支持定制化。

特色優(yōu)勢

01豐富可拓展構(gòu)件庫

豐富可拓展的預定義構(gòu)件庫可用于連續(xù)、離散及混合系統(tǒng)等，適用面廣泛。

02高效易用建模環(huán)境

直觀圖形化建模界面，在統(tǒng)一可視化環(huán)境中采用拖拽的方式進行模型設(shè)計。

03全方位靜態(tài)檢查

基于預定義的設(shè)計規(guī)則判斷模型本身是否存在矛盾，排除開發(fā)早期的模型錯誤。

04動態(tài)仿真與驗證

一鍵動態(tài)仿真調(diào)試與模型驗證、多維度可視化仿真數(shù)據(jù)與驗證結(jié)果反例追溯。

05有效C代碼生成

自動生成符合國軍標8114標準的C代碼，有效減少用戶重復編碼工作。

06國產(chǎn)化環(huán)境支持

支持國產(chǎn)典型操作系統(tǒng)和處理器平臺，為國內(nèi)高端制造領(lǐng)域的嵌入式軟件研制提供支撐平臺。

成果應用

01航空航天

航天航空領(lǐng)域所涉及的飛控等操作系統(tǒng)都極其復雜。相較于傳統(tǒng)的編碼開發(fā)流程，Modeler基于模型的可視化建模開發(fā)，可以覆蓋嵌入式開發(fā)的整個流程，從需求建模、靜態(tài)分析、系統(tǒng)仿真與驗證，再到最終代碼的自動生成，以節(jié)約產(chǎn)品的開發(fā)時間、提高開發(fā)質(zhì)量、減少開發(fā)風險。

02汽車電子

隨著新能源汽車的普及和自動駕駛的興起，行業(yè)對電池管理系統(tǒng)的軟件關(guān)鍵級別要求升級，這就意味著相應軟件驗證成本也急劇加大。Modeler提供基于模型的軟件架構(gòu)建模、仿真、代碼自動生成與測試的完整工具鏈，在極大提升電池管理系統(tǒng)軟件研制效率的同時，節(jié)約高額的研制成本。

03軌道交通

Modeler可視化開發(fā)環(huán)境可以對城軌聯(lián)鎖軟件進行建模，通過使用數(shù)據(jù)流與狀態(tài)機等算子庫，對聯(lián)鎖中的主要邏輯模塊進行建模，并自動生成C代碼。從而為高安全性應用系統(tǒng)的軟件開發(fā)人員提供一套完整的基于模型的開發(fā)解決方案，以此降低開發(fā)成本、縮短開發(fā)周期、減少開發(fā)風險。

審核編輯 黃昊宇