SMAVE MODEL SUITE
模型化嵌入式軟件開發(fā)環(huán)境
SMAVE MODEL SUITE
為安全/任務(wù)關(guān)鍵應(yīng)用量身定制、國產(chǎn)化自主可控的基于模型的設(shè)計、仿真、驗證與代碼自動生成環(huán)境
模型化嵌入式軟件開發(fā)環(huán)境
SMAVE Model Suite為用戶提供關(guān)鍵嵌入式軟件領(lǐng)域的基于模型的開發(fā)環(huán)境，包括基于模型的設(shè)計、自動代碼生成、仿真、模型驗證等功能。通過簡化關(guān)鍵控制應(yīng)用程序設(shè)計、驗證、代碼生成、文檔生成的過程，極大地降低了項目開發(fā)成本，同時增加了項目的正確性與可靠性。
模型化嵌入式軟件開發(fā)環(huán)境
采用高安全模型化建模、分析、代碼生成與驗證技術(shù)，實現(xiàn)可靠系統(tǒng)的高效開發(fā)。
基于模型的軟件開發(fā)方法
■ 以嚴(yán)格的形式化語言為理論基礎(chǔ)
■ 強(qiáng)大的模型表述能力：數(shù)據(jù)流+狀態(tài)機(jī)
■ 模型完整性、確定性保證：強(qiáng)類型語言+靜態(tài)一致性檢查
■ 模型驗證：基于形式化方法的模型檢查技術(shù)
■ 高質(zhì)量和高安全的代碼生成器
■ 圖形化模型仿真與調(diào)試
可以通過不同類型的操作符的組合操作構(gòu)建豐富的模型：
■ 邏輯操作符(Logical)
■ 高階操作符(Higher Order)
■ 數(shù)學(xué)運(yùn)算操作符(Mathematical)
■ 比較操作符(Comparison)
■ 結(jié)構(gòu)/數(shù)組操作符(Structure/Array)
■ 時間操作符(Time)
■ 選擇操作符(Choice)
■ 條件塊操作符(Conditional Block Items)
■ 位操作符(Bitwise)
模型設(shè)計
模型驗證
模型檢查
靜態(tài)一致性檢查
包括命名空間分析、類型分析、時鐘分析、因果關(guān)系分析等多種分析檢查。如果關(guān)系分析可用于驗證同一周期是否存在數(shù)據(jù)流的值依賴自身的值。
模型驗證
模型檢查技術(shù)
■ SMT求解技術(shù) ■ 下推自動機(jī)
有效提高嵌入式系統(tǒng)可靠性
■ 基于模型的開發(fā)方法廣泛的應(yīng)用在航空航天、軌道交通、武器裝備等安全攸關(guān)的領(lǐng)域
■ 增強(qiáng)模型設(shè)計的正確性和安全性
仿真調(diào)試
■ 圖形化模型仿真與調(diào)試 ■ 變量追蹤圖
高質(zhì)量、高安全代碼自動生成
高質(zhì)量和高安全
基于嚴(yán)格的語言理論，保證代碼的運(yùn)行與仿真結(jié)果完全一致
可讀性強(qiáng)
生成代碼具有較強(qiáng)的可讀性，支持針對代碼的修改
代碼可移植
生成的代碼具有可移植性
平臺無關(guān)
生成代碼與平臺無關(guān)
功能可定制
可根據(jù)用戶需求，生成對應(yīng)格式、對應(yīng)規(guī)則的任意語言代碼
平臺支持
支持包括自主可控處理器在內(nèi)的多種CPU
■ Intel & AMD 32位 & 64位 x86處理器（包括海光、兆芯等國產(chǎn)品牌）
■ ARM A8、A9、A53等32位及64位處理器（包括鯤鵬、飛騰、Rockchip、全志等國產(chǎn)品牌）
■ MIPS處理器（包括 龍芯 等國產(chǎn)品牌）
■ 可進(jìn)行多種處理器時間、中斷和內(nèi)存的分析、驗證與仿真
支持包括自主可控處理器在內(nèi)的多種CPU
■ 可生成與國內(nèi)自主可控操作系統(tǒng)適配的應(yīng)用代碼
■ 支持與Linux、VxWorks、QNX等國外主流操作系統(tǒng)集成
■ 支持生成狀態(tài)機(jī)驅(qū)動的零OS代碼（無OS，系統(tǒng)內(nèi)置狀態(tài)機(jī)方式實現(xiàn)）
SMAVE 產(chǎn)品優(yōu)勢
提升效率
■ 圖形化設(shè)計，提高開發(fā)效率
■ 自動生成高安全可直接運(yùn)行代碼
■ 模塊化組件開發(fā)，提高軟件重用性
提高質(zhì)量
■ 基于嚴(yán)格的形式化語言建模，軟件具備確定性
■ 靜態(tài)分析檢查，提前發(fā)現(xiàn)設(shè)計缺陷
■ 模型檢查，驗證需求滿足性
自主可控
■ 自主研發(fā)、擁有自主知識產(chǎn)權(quán)
■ 支持國產(chǎn)操作系統(tǒng)
■ 支持國產(chǎn)處理器硬件
行業(yè)應(yīng)用
