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