行業(yè)背景

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

產(chǎn)品概述

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

產(chǎn)品功能

01圖形化建模

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

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

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

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

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

04運(yùn)行時(shí)驗(yàn)證

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

05代碼自動(dòng)生成

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

06報(bào)告生成與定制

針對(duì)模型靜態(tài)檢查、仿真與調(diào)試、運(yùn)行時(shí)驗(yàn)證等過(guò)程，生成相應(yīng)報(bào)告供用戶查看與存檔，同時(shí)測(cè)試報(bào)告支持定制化。

特色優(yōu)勢(shì)

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

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

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

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

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

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

04動(dòng)態(tài)仿真與驗(yàn)證

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

05有效C代碼生成

自動(dòng)生成符合國(guó)軍標(biāo)8114標(biāo)準(zhǔn)的C代碼，有效減少用戶重復(fù)編碼工作。

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

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

成果應(yīng)用

01航空航天

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

02汽車電子

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

03軌道交通

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

審核編輯 黃昊宇