SCAD Suite控制软件设计软件

概述

SCADE Suite提供基于模型的控制软件建模、验证和自动代码生成的软件开发环境。SCADE Suite基于形式化同步语言scade语言，具备严谨的数学基础，从根本上保证了SCADE软件模型具备精确性、一致性、可验证性、无二义性，以及模型行为的确定性，非常适合高安全关键领域的嵌入式系统软件研制开发。

基于SCADE Suite的软件生命周期

由于从根本上保证了软件模型的确定性，设计人员可以从琐碎的编码工作中解脱出来，更多的关注于软件的需求和业务逻辑设计，改善开发流程，降低开发成本，提高效率和最终软件产品的安全性可靠性。

结构化设计

SCADE模型高度模块化，层次清晰，接口明确，体现了高内聚低耦合的设计思想，有利于软件设计人员自顶向下逐层设计、并发设计、模型变更和维护。

SCADE Suite 建模

SCADE Suite集成开发环境提供了图形化的建模方式，以建立基于scade形式化语言的模型，支持数据流和安全状态机，使得SCADE模型容易理解的同时，软件设计工作更加流畅和高效。

SCADE Suite 模型设计验证

SCADE Suite支持对模型设计进行一系列验证，以确保模型和需求的一致性。包括：

● SCADE模型的语法语义检查

● 用户自定义的设计规则检查

● 模型到需求的追溯分析

● 模型动态行为仿真及调试

● 形式化验证

● 时间和堆栈分析

● 模型覆盖率分析

模型语法语义检查

SCADE Suite支持模型的静态检查，帮助设计人员在开发的早期就排除模型中的错误。

用户自定义的设计规则检查

SCADE Suite 提供了模型设计规则检查的基本框架，可直接使用，也可由客户通过开放的API接口根据自生需要进行定制，非常灵活。

模型到需求的追溯分析

通过SCADE Lifecycle ALM Gateway支持对软件需求、SCADE模型、测试用例等进行追踪分析，满足高安全关键软件研制开发流程的要求。

模型动态行为仿真及调试

SCADE Suite模型调试支持单步、多步、回退及连续运行，在图形上可以很方便观测模型的执行过程以及各数据流上的值。SCADE Suite还支持和人机交互界面进行联合调试，支持仿真调试过程的场景录制和回放。

形式化验证

由于SCADE模型是形式化模型，可以应用数学分析的方法验证模型的安全属性。SCADE Suite支持模型检测的方法遍历软件模型所有的状态空间，以分析证明软件模型满足安全属性。模型检测的方法基于严谨的数学理论，自动执行高效率分析，是模型动态行为测试的有效补充。

SCADE Suite内置了两个形式化验证功能：除零检查和溢出检查，可以帮助设计人员快速定位可能出现的除零隐患和溢出风险。

时间和堆栈分析

SCADE Suite支持对模型最坏运行时间与堆栈使用情况进行分析。基于这些信息，设计人员可以获得SCADE模型工程中各个模块的占用时间和空间的量化分析结果，发现造成性能瓶颈的设计模型，从而给模型优化提供重要的线索，有针对性的改善和提高SCADE模型的性能。

安全代码生成

SCADE Suite KCG代码生成器从SCADE模型自动生成C代码或Ada代码，并且保证了代码和模型的一致性。SCADE Suite KCG生成的代码满足高安全性的要求，代码效率高，可以直接进行工程应用，从而省去了繁琐的编码和代码验证工作。

支持基于多核架构及多速率组的应用软件

SCADE Suite KCG可以支持生成基于多核架构设计以及多速率组的嵌入

式软件安全代码，可以通过可定制的代码生成适配器实现和不同操作系

统的集成，目前支持的目标平台包括:

● Pthread win32

● Infineon Aurix / HighTec

● MPPA Kalray

● PikeOS SYSGO

系统、软件、代码、文档的一致性

通过SCADE Suite KCG安全代码生成，SCADE开发环境确保了从系统架构、软件模型、实现代码的同步和一致性。借助于SCADE LifeCycle Reporter文档生成器，设计文档自动生成，并保持了和设计的一致性。

编译器验证包

编译器验证包（CVK：Compiler Verification Kit）包含了所有SCADE代码生成器所能生成的C代码子集，以及一套与之对应的具备相当复杂度的测试用例。CVK可用于验证目标编译器能正确编译所有SCADE Suite代码生成器所生成的代码，增加对编译器的信心；同时CVK定义的C语言子集可用于验证源代码和目标码之间的一致性，从而满足高安全软件研制标准中对最高安全等级软件所要求实现的源代码到目标代码一致性的目标。