SCADE——一个高安全性的应用开发环境（一）
Safety-Critical Application Development Environment
Overview
SCADE是一个高安全性的应用开发环境，是法国爱斯特尔技术公司运用基于模型的方式为高安全性系统提供的完整的解决方案，能自动生成满足安全特性的嵌入式代码，在航空、航天、国防以及核工业等安全领域都有广泛的应用。
SCADE 建立在同步编程的概念之上，以Lustre语言为核心，内置了 Prover-Technology公司的 Prover（SAT-based）工具，实现了子啊模型级进行形式化验证的功能。它提供了两套机制( 数据流和安全状态机) 来进行图形化建模。这两套机制具有严格的数学语义，它们能够保证设计模型的精确性、完整性、一致性和无二义性。
SCADE覆盖了从需求到代码的所有开发流程，包括需求管理、需求建模、模型检查、模拟仿真、测试覆盖率分析、形式化验证、代码生成、文档生成等。
Product
SCADE Suite: 适用于控制软件的逻辑建模。通过采用SCADE语言和统一的形式化语义，可实现基于模型的设计、仿真、验证、认证级代码生成以及与其他开发工具和平台的交互。
SCADE Display: 新一代图形软件开发平台，是一套灵活的面向高安全性图形显示和HMLs的设计与开发环境。可完成原型生成、设计仿真、验证和认证级代码生成等。
SCADE LifeCycle: 帮助系统和软件开发人员进行产品的生命周期管理。主要功能包括需求和可追溯性管理工具、符合DO-178B标准的认证计划模板以及自动化文档生成器。
SCADE System: 基于SysML语言和Eclipse标准，联接SCADE Suite、SCADE Display、SCADE LifeCycle，在同一架构下工作从而避免重复劳动以及系统结构和软件行为定义之间的偏差。
SCADE ARINC 661: 业内唯一的、以基于模型的方式完全实现ARINC 661标准版本4和版本5中定义的所有控件的解决方案。基于现有的SCADE产品模块，提供基于“所见即所得”的UA页面定制、Server端widget定制以及通信代码的生成，确保运行时和定制时看到的外观一致。同时，开发人员可以在SCADE Suite中对UA端逻辑与Server端Widgets属性或事件进行绑定和映射，实现对UA端控制逻辑与Server端图形页面（DF文件）的联合仿真。
Formal verification
- 提取可处理的安全性需求；
- 通过数据流图描述抽象出来的软件安全性需求；
- 构建验证环境。将形式化的软件需求描述与安全性需求描述（使用SCADE模型）结合。
- 调用形式化验证引擎进行分析。形式化验证引擎的目标是：在所有的周期中，在所有可能的测试场景下，系统都能够满足安全性特性。如果系统满足这样的安全性特征，则会给出一个证明，否则给出一个反例帮忙分析。
