●前言
章 開啟SCADE之旅
1.1 背景概念簡介
1.1.1 嵌入式繫統
1.1.2 安全關鍵繫統
1.1.3 機載軟件的適航標準
1.1.4 基於模型的開發與驗證
1.2 SCADE介紹
1.2.1 同步語言介紹
1.2.2 SCADE產品的演進
1.2.3 SCADE Suite的特點
1.2.4 SCA：DE產品未來發展的路線圖
1.3 SCADE快速入門
1.3.1 SCADE的適用環境和安裝步驟
1.3.2 創建SCADE Suite工程
1.3.3 SCADE Suite操作符和輸入輸出的創建
1.3.4 飛機滾轉角示例
練習題
第2章 SCADE Suite建模基礎
2.1 SCADE Suite集成開發環境常見操作
2.2 SCADE數據類型
2.2.1 預定義數據類型
2.2.2 自定義數據類型
2.3 常量
2.3.1 常量的定義
2.3.2 常量的使用
2.4 操作符
2.4.1 預定義操作符
2.4.2 自定義操作符
2.5 條件模塊
2.5.1 條件模塊的概念
2.5.2 條件模塊的創建與編輯
2.5.3 條件模塊中變量的隱式賦值
2.6素
2.6.1 導入常量
2.6.2 外部引用變量（Sensor）
2.6.3 導入操作符
2.6.4 導入靜態庫
練習題
第3章 SCADE Suite安全狀態機
3.1 安全狀態機
3.1.1 狀態機的組成
3.1.2 狀態機的創建
3.2 狀態的設置
3.2.1 狀態
3.2.2 初始狀態和終止狀態
3.2.3 狀態的編輯
3.3 遷移的設置
3.3.1 遷移
3.3.2 遷移的條件和行為
3.3.3 遷移的觸發
3.3.4 遷移和初始狀態
3.3.5 遷移的編輯
3.4 狀態機中變量的隱式賦值
3.4.1 變量的隱式賦值
3.4.2 定義變量的Last值
3.4.3 定義變量的Default值
3.4.4 同時定義變量的Last值和Default值
3.4.5 同時不定義變量的Last值和Default值
3.5 Signal（信號量）
練習題
第4章 SCADE Suite不錯建模設計
4.1 數組操作
4.1.1 數組的創建
4.1.2素的獲取
4.1.3 數組操作
4.2 結構體操作
4.2.1 Data Structure操作符
4.2.2 Make操作符
4.2.3 Flatter操作符
4.2.4 Project操作符
4.3 迭代器建模
4.3.1 迭代器的創建和循環次數設置
4.3.2 map迭代器
4.3.3 fold迭代器
4.3.4 mapfold迭代器
4.3.5 mapi迭代器
4.3.6 foldi迭代器
4.3.7 mapw迭代器
4.3.8 foldw迭代器
4.3.9 mapwi迭代器
4.3.1 0foldwi迭代器
4.3.1 1mapfoldi迭代器
4.3.1 2mapfoldw迭代器
4.3.1 3mapfoldwi迭代器
4.4 條件激活操作
4.4.1 條件激活操作符的創建
4.4.2 Boolean Activate操作符
4.4.3 Restart操作符
4.5 多態建模
4.5.1 數組大小的參數化
4.5.2 變量類型的參數化
4.5.3 操作符行為的參數化
4.6 仿真相關的設置
4.6.1 Assume和Guarantee
4.6.2 精度的設置
練習題
第5章 SCADE Suite基於模型的驗證
5.1 基於SCADE Suite模型的驗證流程
5.1.1 DO-178C的傳統驗證手段
5.1.2 基於SCADE Suite模型的驗證工作
5.2 基礎驗證活動
5.2.1 SCADE模型檢查器
5.2.2 SCADE模型仿真
5.2.3 SCADE覆蓋分析
5.3 認證級測試環境QTE
5.3.1 SCADE QTE的工作流
5.3.2 創建測試工程
5.3.3 設計仿真用例和仿真規程
5.3.4 QTE在主機上的功能測試
5.3.5 QTE在主機上的模型覆蓋分析
5.3.6 QTE在主機上的代碼覆蓋分析
5.3.7 QTE在目標機上的測試
5.3.8 QTE下多操作符驗證的注意事項
5.3.9 仿真結果的評審
5.4 SCADE的形式化驗證
5.4.1 安全屬性
5.4.2 形式化驗證的工作流
5.4.3 形式化驗證工具Design Verifier
5.4.4 形式化驗證實例
5.5 SCADE編譯器驗證套件
5.5.1 編譯器的驗證
5.5.2 C語言安全子集
5.5.3 CVK的內容與使用方法
5.5.4 使用SCADE CVK的注意事項
練習題
第6章 代碼和其他目標的生成
6.1 代碼生成
6.1.1 代碼生成的配置
6.1.2 單個操作符的代碼生成配置
6.1.3 創建並保存自定義配置
6.2 代碼集成
6.2.1 代碼生成步驟
6.2.2 生成代碼的集成
6.2.3 代碼集成的其他考慮
6.3 Simulink的S函數生成
6.4 NI VeriStand生成
6.5 FMU生成
6.5.1 Modelica協會與統一建模語言
6.5.2 FMI標準與FMU文件
6.5.3 Suite生成FMU文件
6.6 Adaptor生成
6.7 設計文檔生成
練習題
第7章 SCADE Suite模型的優化
7.1 模型優化的目標和基準
7.1.1 安全關鍵繫統的軟件規模在增長
7.1.2 MBDV方法的優勢
7.1.3 模型優化的目標和準則
7.2 布局格式優化
7.2.1 布局格式的推薦規範
7.2.2 編輯技巧
7.2.3 自定義樣式
7.3 模型優化
7.3.1 模型優化的內容和要點
7.3.2 模型優化示例
7.4 最壞運行時間與堆棧分析
7.4.1 TSO介紹
7.4.2 TSO使用方法
7.5 性能優化案例
7.5.1 算法一：基於過程的傳統C語言編程的思維
7.5.2 算法二：優化的基於過程的思維
7.5.3 算法三：選擇恰當的迭代子
7.5.4 算法四：關注數據的SCADe Suite建模很好方式
7.5.5 WCET分析結果
7.5.6 堆棧分析結果
練習題
第8章 項目管理
8.1 項目組織
8.1.1 命名規則
8.1.2 工程管理
8.1.3 文件管理
8.2 追蹤管理
8.2.1 DO-178C中追蹤管理的要求
8.2.2 SCADE RM Gateway
8.2.3 普通文本類型文件的追蹤
8.2.4 SCADE文件的追蹤
8.2.5 驗證相關文檔的追蹤
8.2.6 生成快照
8.2.7 生成追蹤矩陣
8.3 配置管理
8.4 建模規範
練習題
第9章 綜合案例
9.1 目標
9.2 中位數計算設計實例
9.2.1 Torben算法求中位數簡述
9.2.2 實例創建步驟
附錄1 縮略詞彙總和常用詞定義
附錄2 SCADE Suite關於DO-178C／DO-331目標的符合性矩陣
參考文獻
