第1章 开启SCADE之旅 1
1.1 背景概念简介 1
1.1.1 嵌入式系统 1
1.1.2 安全关键系统 1
1.1.3 机载软件的适航标准 2
1.1.4 基于模型的开发与验证 6
1.2 SCADE介绍 8
1.2.1 同步语言介绍 8
1.2.2 SCADE产品的演进 11
1.2.3 SCADE Suite的特点 14
1.2.4 SCADE产品未来发展的路线图 17
1.3 SCADE快速入门 18
1.3.1 SCADE的适用环境和安装步骤 18
1.3.2 创建SCADE Suite工程 23
1.3.3 SCADE Suite操作符和输入输出的创建 26
1.3.4 飞机滚转角示例 27
练习题 35
第2章 SCADE Suite建模基础 36
2.1 SCADE Suite集成开发环境常见操作 36
2.2 SCADE数据类型 38
2.2.1 预定义数据类型 38
2.2.2 自定义数据类型 38
2.3 常量 46
2.3.1 常量的定义 46
2.3.2 常量的使用 47
2.4 操作符 48
2.4.1 预定义操作符 49
2.4.2 自定义操作符 63
2.5 条件模块 64
2.5.1 条件模块的概念 64
2.5.2 条件模块的创建与编辑 65
2.5.3 条件模块中变量的隐式赋值 68
2.6 导入元素 70
2.6.1 导入常量 71
2.6.2 外部引用变量（Sensor） 72
2.6.3 导入操作符 73
2.6.4 导入静态库 79
练习题 81
第3章 SCADE Suite安全状态机 82
3.1 安全状态机 82
3.1.1 状态机的组成 82
3.1.2 状态机的创建 84
3.2 状态的设置 85
3.2.1 状态 85
3.2.2 初始状态和终止状态 85
3.2.3 状态的编辑 86
3.3 迁移的设置 89
3.3.1 迁移 89
3.3.2 迁移的条件和行为 89
3.3.3 迁移的触发 91
3.3.4 迁移和初始状态 91
3.3.5 迁移的编辑 91
3.4 状态机中变量的隐式赋值 98
3.4.1 变量的隐式赋值 98
3.4.2 定义变量的Last值 99
3.4.3 定义变量的Default值 100
3.4.4 同时定义变量的Last值和Default值 101
3.4.5 同时不定义变量的Last值和Default值 102
3.5 Signal（信号量） 104
练习题 105
第4章 SCADE Suite高级建模设计 106
4.1 数组操作 106
4.1.1 数组的创建 106
4.1.2 数组元素的获取 108
4.1.3 数组操作 110
4.2 结构体操作 112
4.2.1 Data Structure操作符 112
4.2.2 Make操作符 113
4.2.3 Flatter操作符 113
4.2.4 Project操作符 114
4.3 迭代器建模 114
4.3.1 迭代器的创建和循环次数设置 115
4.3.2 map迭代器 116
4.3.3 fold迭代器 117
4.3.4 mapfold迭代器 117
4.3.5 mapi迭代器 122
4.3.6 foldi迭代器 124
4.3.7 mapw迭代器 125
4.3.8 foldw迭代器 126
4.3.9 mapwi迭代器 128
4.3.10 foldwi迭代器 130
4.3.11 mapfoldi迭代器 131
4.3.12 mapfoldw迭代器 133
4.3.13 mapfoldwi迭代器 135
4.4 条件激活操作 136
4.4.1 条件激活操作符的创建 137
4.4.2 Boolean Activate操作符 137
4.4.3 Restart操作符 140
4.5 多态建模 141
4.5.1 数组大小的参数化 141
4.5.2 变量类型的参数化 142
4.5.3 操作符行为的参数化 143
4.6 仿真相关的设置 146
4.6.1 Assume和Guarantee 146
4.6.2 精度的设置 147
练习题 148
第5章 SCADE Suite基于模型的验证 149
5.1 基于SCADE Suite模型的验证流程 149
5.1.1 DO-178C的传统验证手段 149
5.1.2 基于SCADE Suite模型的验证工作 152
5.2 基础验证活动 156
5.2.1 SCADE模型检查器 156
5.2.2 SCADE模型仿真 157
5.2.3 SCADE覆盖分析 167
5.3 认证级测试环境QTE 182
5.3.1 SCADE QTE的工作流 182
5.3.2 创建测试工程 183
5.3.3 设计仿真用例和仿真规程 184
5.3.4 QTE在主机上的功能测试 193
5.3.5 QTE在主机上的模型覆盖分析 197
5.3.6 QTE在主机上的代码覆盖分析 201
5.3.7 QTE在目标机上的测试 203
5.3.8 QTE下多操作符验证的注意事项 205
5.3.9 仿真结果的评审 208
5.4 SCADE的形式化验证 208
5.4.1 安全属性 208
5.4.2 形式化验证的工作流 208
5.4.3 形式化验证工具Design Verifier 209
5.4.4 形式化验证实例 210
5.5 SCADE编译器验证套件 218
5.5.1 编译器的验证 218
5.5.2 C语言安全子集 219
5.5.3 CVK的内容与使用方法 220
5.5.4 使用SCADE CVK的注意事项 222
练习题 223
第6章 代码和其他目标的生成 224
6.1 代码生成 224
6.1.1 代码生成的配置 224
6.1.2 单个操作符的代码生成配置 240
6.1.3 创建并保存自定义配置 242
6.2 代码集成 242
6.2.1 代码生成步骤 242
6.2.2 生成代码的集成 243
6.2.3 代码集成的其他考虑 245
6.3 Simulink的S函数生成 245
6.4 NI VeriStand生成 247
6.5 FMU生成 249
6.5.1 Modelica协会与统一建模语言 249
6.5.2 FMI标准与FMU文件 249
6.5.3 Suite生成FMU文件 250
6.6 Adaptor生成 252
6.7 设计文档生成 253
练习题 258
第7章 SCADE Suite模型的优化 259
7.1 模型优化的目标和基准 259
7.1.1 安全关键系统的软件规模在增长 259
7.1.2 MBDV方法的优势 261
7.1.3 模型优化的目标和准则 261
7.2 布局格式优化 264
7.2.1 布局格式的推荐规范 264
7.2.2 编辑技巧 267
7.2.3 自定义样式 276
7.3 模型优化 280
7.3.1 模型优化的内容和要点 280
7.3.2 模型优化示例 281
7.4 最坏运行时间与堆栈分析 290
7.4.1 TSO介绍 290
7.4.2 TSO使用方法 291
7.5 性能优化案例 296
7.5.1 算法一：基于过程的传统C语言编程的思维 296
7.5.2 算法二：优化的基于过程的思维 299
7.5.3 算法三：选择恰当的迭代子 301
7.5.4 算法四：关注数据的SCADE Suite建模最佳方式 303
7.5.5 WCET分析结果 305
7.5.6 堆栈分析结果 305
练习题 306
第8章 项目管理 307
8.1 项目组织 307
8.1.1 命名规则 307
8.1.2 工程管理 307
8.1.3 文件管理 311
8.2 追踪管理 312
8.2.1 DO-178C中追踪管理的要求 312
8.2.2 SCADE RM Gateway 313
8.2.3 普通文本类型文件的追踪 318
8.2.4 SCADE文件的追踪 333
8.2.5 验证相关文档的追踪 335
8.2.6 生成快照 338
8.2.7 生成追踪矩阵 339
8.3 配置管理 341
8.4 建模规范 343
练习题 343
第9章 综合案例 344
9.1 目标 344
9.2 中位数计算设计实例 344
9.2.1 Torben算法求中位数简述 344
9.2.2 实例创建步骤 345
附录1 缩略词汇总和常用词定义 358
附录2 SCADE Suite关于DO-178C/DO-331目标的符合性矩阵 360
参考文献 367