新闻  |   论坛  |   博客  |   在线研讨会
SCADE介绍
tongxin | 2009-03-20 14:56:50    阅读:19090   发布文章

sCADE是英文 Safety-Critical Application Development Environment的缩写,它是一个高安全性的应用开发环境。
%A   法国爱斯特尔技术公司在开发SCADE软件时联合了航空电子、汽车电子、军用飞机以及核电站控制等领域的合作伙伴,如AIRBUS, Schneider Electric, Dassault Aviation和THALES等,综合了多个领域对嵌入式软件开发的不同要求,提出了一整套高安全性嵌入式软件开发的自动化工具和相应方法学。   
%A   SCADE运用了correct by construction的概念,覆盖了嵌入式软件开发中从需求到嵌入式代码的整个流程:需求建模、模型检查、模拟仿真、形式验证、嵌入式代码自动生成、以及文档自动生成等等。除此之外,它还与许多其它工具进行了桥接。下面,我们从这二个方面来分别介绍SCADE的功能模块。
%A
%A 从需求到代码
%A
%A  图形化建模
%A
%A
%A   实时高安全性软件设计工具SCADE通过图形化建模来实现软件开发的自动化,将用户从冗长枯燥的任务中解放出来,有更多的时间去关注其他更重要的领域。
%A   SCADE编辑器提供了二套机制来进行图形化建模:数据流图和有限状态机。这二套机制都建立在严格的数学模型基础之上,具有严格的数学语义,它们保证了设计模型的精确性、完整性、一致性、无二义性。这些都是高安全性系统的基本特性。
%A   
%A   数据流机制适合连续性系统的建模,有限状态机则适合于离散性系统的建模。SCADE把这二套机制很好地融合在一起,使得能够适合于不同类型的系统尤其是混合系统的开发。
%A   SCADE的图形化编辑器界面友好,易学易用,有助于系统设计组同软件设计组之间的交流,从而缩短产品开发时间。
%A   
%A   在图形化建模后,我们可以对建立的模型进行检查:对模型中的不一致、类型不匹配、数据回路等所有的模型错误,SCADE都能以超文本的方式进行定位,以便纠错。
%A   模型检查有两种形式:局部模式检查我们选中的类型块、常量块或者操作符;全局模式检查整个模型。
%A
%A 模拟仿真
%A
%A
%A   在系统建模后,我们可以对整个系统或是系统中任意一个模块进行模拟仿真。仿真器是基于SCADE生成的代码进行仿真的,它是一个强大的可视化的图形调试工具,可以设置断言、断点、中断条件;可以检查输入数据、内部的变量和输出数据的值;还可以记录和回放仿真的场景(scenario)。仿真器的输入输出可以用文本或表格的形式给出,还可以由著名的TCL语言来驱动。
%A   对于一个拥有大量输入输出的系统来说,我们在仿真的时候,可能只对系统中的若干个信号的变化感兴趣。SCADE工具能够很方便地把我们感兴趣的信号集中在一起,并用图形的方式记录仿真时这些信号的变化情况,以便于检查。
%A    SCADE还提供了良好的接口,供用户根据实际的应用,设计友好的仿真面板。
%A
%A 形式验证
%A   
%A
%A   模拟和仿真能够在一定程度上测试系统的模型是否很好实现我们所期望的功能,但是,它不能保证系统是否做了预期外的不应该做的事情。因此,只经过模拟仿真测试的系统安全性并不能完全得到保证。SCADE内置的形式验证的功能解决了这个问题。
%A   详尽的形式验证,既不需要执行模型,也不需要借助测试向量,就可以检验SCADE模型是否达到安全性、可靠性和其他方面的要求。SCADE的 Prover插件将Prover公司的最新科技集成SCADE图形界面中,设计好了系统的安全性要求和一个“特性观察器”之后,用户只需按一个键就可验证 SCADE的模型的安全性。如果模型是安全的,它能给出一个安全的证明;如果模型是不安全的,它能给出一个反例,而这个反例又可以在仿真器中调出来进行仿真,以详细地观察系统是怎样一步步地进入不安全状态的。形式验证的这一功能在很大程度上方便了系统的纠错,同时保证了目标系统的安全性。
%A
%A 嵌入式代码的自动生成
%A
%A
%A   经过仿真和形式验证,保证了模型的安全性以后,SCADE可以自动生成面向工程的ANSI C或Ada 83/95语言的嵌入式代码。
%A   它生成的代码满足一系列的安全性特征,例如,有界的堆栈,没有动态指针,没有递归调用,没有死代码等等。另外,SCADE自动生成的代码的运行空间和运行时间与手写代码基本相当,但比手写代码更易于维护和调整。
%A    和其它的许多代码生成器相比,SCADE代码生成有二个显著的特点。第一,SCADE所生成的代
%A 码完全面向工程,可以直接嵌入到所开发的系统中去而不需要做任何修改。第二,SCADE基于严格的数据理论,它保证所生成的代码的正确性,并承诺所生成的代码的行为和仿真的行为完全一致。这二点是很多代码生成器所做不到的。
%A
%A KCG
%A
%A   民航系统的开发流程必须满足DO-178B国际标准。KCG是爱斯特尔技术公司提供的满足DO-178B民航A级安全标准的代码产生器。由于KCG本身满足这一标准并保证了代码的正确性,它不仅大大节省了编码工作,而且完全免去了代码的单元测试,很大程度地节省了验证工作和验证时间。(详见第三章 KCG和 DO-178B标准) KCG的使用对空中客车(AIRBUS)的A340/500项目和欧洲直升机(Eurocopter)的EC135、EC155等项目的开发和质量认证带来巨大的帮助。
%A
%A 与其它工具的桥接
%A
%A 与DOORS的桥接
%A
%A   DOORS是一个需求分析和追踪的工具。SCADE和DOORS的桥接工具可以把一个SCADE模型自动地输入到DOORS环境中,以便于需求分析和追踪,使SCADE中的设计与需求,测试计划和其他模型或文档联系起来。
%A   在需求分析和追踪的过程中,如果我们想了解DOORS中的一个对象对应于SCADE中的哪个实体,该桥接工具还提供了定位的功能。只需点击一个按钮,它就会启动SCADE,调出相应的SCADE模型,并把光标定位在相应的实体上。
%A
%A 与配置管理工具的桥接
%A
%A   SCADE以ASCII格式保存所有数据,并支持SCCI标准的配置管理界面。因此,SCADE可以很方便地与所有支持SCCI标准的配置管理工具进行桥接,如Telelogic Synergy,MERANT PVCS,
%A Rational Clearcase以及Wincvs等等。SCADE编辑器中还集成了常用的版本管理命令,如checkin,checkout等等。
%A
%A 与Simulink的桥接
%A
%A   如果您在以往的开发过程中,使用Matlab/Simulink做控制率设计,那么SCADE与 Simulink的桥接能给您很大帮助。该桥接工具可以把Simulink模型中我们所需要的软件模块自动转化成一个Scade模型,这一方面帮助我们重用现有的模型和设计,减少工作量;另一方面也又能使我们充分享受SCADE的相对优势,如确定性的系统行为、形式验证、嵌入式代码的自动生成等等。此外,该桥接还可以把SCADE生成的代码返回到Simulink模型内部作为一个S函数,这样可以进行软件代码在其运行环境中模拟仿真。
%A
%A
%A%A
%A

*博客内容为网友个人发布,仅代表博主个人观点,如有侵权请联系工作人员删除。

参与讨论
登录后参与讨论
fred0216  2011-05-06 17:31:26 

您好,请问如何可以得到这个开发平台呢?

最近文章
寂寞如雪
2009-05-19 19:01:18
夜色花
2009-05-19 18:56:22
没有爱可以重来
2009-05-19 18:54:59
推荐文章
最近访客