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