SCADE 开发环境介绍

SCADE Suite 中的"SCADE"为"安全关键应用开发环境"的缩写。需说明的是，在时效性方面，下面的描述反映的是发展至2010年左右的情况。更详细的内容，可参考《Formal Methods - Industrial Use from Model to the Code》(ISBN 978-1-84821-362-3)。

SCADE 开发环境提供了基于 SCADE 建模语言的工具集，覆盖了软件应用研发活动中的设计、编码与验证阶段工作。SCADE 开发环境能够研发软件应用的两部分内容，一部分为功能性部分、一部分为图形化交互或展示部分。对功能性部分，由 SCADE Suite 部分的工具提供支持；对图形化交互或展示部分，由 SCADE Display 部分的工具提供支持。这里将集中描述 SCADE Suite 部分的内容。

SCADE 开发环境的核心是 SCADE 编辑器，通过 SCADE 编辑器能够编辑结构化的模型。模型仿真、模型测试覆盖率、形式化方法引擎提供了在研发活动推进到代码编程前的模型验证方法。KCG作为有资质的代码生成器能够生成与模型含义一致的代码，这不仅节省了代码编程工作，也节省了与代码编程配套的模块化测试工作。

下面将从模型验证、性能预测、KCG 代码生成三部分介绍 SCADE Suite 开发环境。

模型验证

SCADE 模型验证的目标为确保 SCADE 开发的应用与高层次需求保持一致，不会引入预期之外的功能。

模型与需求的关联检查

模型验证方法的组成之一为模型与需求的关联检查。通过这项检查，可以验证 SCADE 模型是否与上游的相应需求对应。用于这项工作的 SCADE 工具是 “SCADE Suite 需求管理网关”（RM Gateway）。该工具可以将 SCADE 模型与高层次需求进行关联，计算 SCADE 模型覆盖需求的百分比；以及计算当需求更改后，对 SCADE 模型的影响分析。

模型仿真器

在其余的验证阶段中，SCADE 模型最重要的属性是模型的可执行性。对模型的功能验证，可通过 “SCADE Suite 仿真器”对模型进行执行与调试。仿真的优点在于，模型在仿真中运行的结果，与由模型生成的代码在目标环境中运行的结果是相同的。

模型覆盖

SCADE 模型的结构化覆盖率可通过 “SCADE Suite 模型测试覆盖”（MTC, Model Test Coverage）工具进行计算。通过该工具，可以在研发过程的较早阶段，发现测试过程中不可达的模型。

模型形式化验证

除了基于对SCADE 模型测试的验证手段外，SCADE 还提供集成源自 Prover Technology 的 Prover 插件的 SCADE Suite 设计验证器(DV)。该工具能对 SCADE 模型实施模型检测形式化技术，从而验证 SCADE 模型是否符合高层次需求。

形式化验证技术提供了一种数学框架去推导系统行为。在 SCADE 模型的基础上，DV 用户可以通过 SCADE 模型的形式，去描述安全性质，再使用 DV 进行形式化验证。之后 DV 会对可能的系统行为进行穷尽式地数学分析。对每一条安全性质，通过 DV 验证，会有两种可能性结果。一种为应用模型符合给定性质；另一种为对某些输入，应用模型不符合给定性质。对后一种情况，DV 会提供导致模型执行错误的输入场景。

性能预测

SCADE 产品集成了 SCADE Suite 时序与栈分析器（Timing and Stack Verifier, TSV）。对 SCADE 模型生成的C程序，该工具可以对给定硬件目标上执行C程序的最长时间进行估计，并对最大栈空间使用进行估计。该工具集成了 AbsInt 开发的 aiT 工具对静态分析技术提供支持。