白皮书

来自于2008年ERTS大会

SCADE6 基于模型的高安全性软件解决方案

作者：François-Xavier DORMOY, 爱斯特尔公司SCADE研发经理

摘要

SCADE Version 6既是一种语言，也是一个高安全性软件开发环境，它提供了一种全新的统一建模方式，包含了从系统需求到软件工程的整个过程。整个过程的基础就是在每一步都保证安全性，SCADE让工程师将精力集中在关键问题上，省去了大量的开发工作量。

SCADE6是基于模型的工具，能满足工程师所需，并实现D0178-B, EN50128或IEC 61508所规定的高安全性标准。

本文介绍了SCADE6并说明了在语言定义，建模环境及代码生成过程中的关键因素，意在实现一个高安全性的开发流程。

» 点击获取全文 «

来自于2008年ERTS大会

经验证的多任务，多频率同步系统构架

作者：Jean-Louis CAMUS – 爱斯特尔公司高级咨询，Pierre VINCENT -爱斯特尔公司咨询，Olivier GRAFF - Intertechnique, Sébastien POUSSARD – Intertechnique

摘要

基于模型的同步软件开发技术对于开发高安全性实时软件是严格有效的。当前，同步技术常常运用在单一任务或者局部同步全局不同步的多任务调用中。本文介绍一种能实现多频率任务的技术，该技术同时还保留了同步方法的确定性与可验证性。我们的方法使用同步框架来确保准确与可验证性，并将整个同步模型的不同部分以一个简单有效的结构来实现。这样的构架既确保了在运行时的确定性，也可通过仿真与形式验证对整个模型进行验证。这个构架已经应用于实际航空设备中的软件部分。本文中还涉及到了其他观点。

» 点击获取全文 «

来自于2008年ERTS大会

将高安全性系统的高层设计工具与可执行程序的WCET分析工具相结合

作者：Reinhold HECKMANN - Absint, Christian FERDINAND - Absint, Florian MARTIN - Absint, Thierry LE SERGENT - SCADE 爱斯特尔产品经理，Bruno MARTIN - 爱斯特尔研发经理，Xavier FORNARI -爱斯特尔研发经理，Daniel LOPES - 爱斯特尔研发工程师

摘要

使用类似于SCADE Suite的自动代码生成器对基于模型的软件需求生成代码，能够在项目早期就进行设计验证，避免编码错误，减少单元测试。诸如执行时间，内存损耗等非功能性属性需要专门的分析。象AbsInt的StackAnalyzer与时间分析器aiT这样的静态程序分析工具能很好地完成对这些性能的验证。这些工具也能就当前设计对资源的损耗给SCADE用户一个直接的反馈，从而帮助用户寻找一些更加有效的实现方式。SCADE，StackAnalyzer与 aiT相结合，能够在SCADE开发环境中直接获取基于生成代码的分析结果。我们将介绍这些工具，他们的集成，当前的结果以及与其他分析工具的集成计划。

» 点击获取全文 «

基于OCaml的认证级开发工具实现

作者：Bruno Pagano, Olivier Andrieu, Benjamin Canou, Emmanuel Chailloux, JeanLouis ColaÃ§o, Thomas Moniot and Philippe Wang

摘要

本文介绍了从使用OCaml语言进行高安全性软件开发工具的实现中得到的反馈。OCaml语言现在已用于新一代的ScadeTM认证级嵌入式代码生成器。实现工具的要求相对嵌入式代码来说要低一些。但是，它们仍旧是高要求的，并且要求一些强制性语言的特性用于此类开发。使用OCaml语言的效果相当显著：首先是它的高层特点（高阶功能语言，参数多态性，样式匹配），二是它的底层机制，这是实时系统所需的。为了开发用以检查高安全性软件开发过程的工具，必须先将这些检查项用OCaml语言来解释，然后通过调整直至满足要求。在此，我们建议要对该语言有一些限制，相应的实时库也要简化，这样我们就能按照MC/DC标准来定义OCaml程序的覆盖率，并进行定量。我们能预见这种语言将在工业环境下流行起来，同时为认证级代码的生成工具提供更高的理念与实现手段。

Certified Development Tools Implementation in Objective Caml. In Practical Aspects of Declarative Languages, 2008. Lecture Notes in Computer Science, vol. 4902, pp. 2-17. http://dx.doi.org/10.1007/978-3-540-77442-6_2 © Springer-Verlag Berlin Heidelberg 2008

» 点击获取全文 «

摘自于2006年德国航空航天大会

用于轨道交通行业高安全性应用的开放软件开发平台

作者：Jakob Gärtner, 爱斯特尔高级咨询

摘要

从前，世界是理想化的。每一个国家的轨道交通公司都有自己的轨道车辆，信号系统以及通讯系统的供应商。他们有自己的信号标准，自己的轨道宽度。对于专门的供应商而言，这就意味着他可完全依靠他与客户之间的关系，不必害怕任何的竞争。这样静态的带有保护主义色彩的市场将导致我们的体系结构，商业模式以及发展过程变得相当传统，停滞不前，及其顽固。

»点击获取全文 «

摘自2006年SpaceOps

United Space Alliance

作者：William T. Smithgall

摘要

支持任务目标的标准化硬件组件已经开发并加以整合，集成空间运行需要这些组件的并行处理。飞行控制软件是一个关键性部件，必须按照任务不同而作调整，使得飞行器与载荷完成不同的任务。用一个标准化的飞行控制单元来完成这个运行需求，如果用现有的开发手段是相当困难的。先进的自动化软件工具能够省去大量高强度的手工劳动，与传统方法相比更加切实有效。本文介绍了飞行控制软件的自动开发与维护过程，不仅满足了任务的自定义，后期产品的改进，也较好地满足了及时交货与集成目标。从当前的宇宙飞船飞行控制软件开发过程中我们可以看到节约资源的机会。

»点击获取全文«

摘自2006年ERTS

UML与高安全性软件开发环境的桥接

作者：Alain Le Guennec, Bernard Dion

摘要

本文介绍了一种方法，能将UML与SCADE的长处相结合，用以开发高安全性系统。运用UML可以描述系统的高层需求与体系结构，SCADE可用于描述软件行为，我们提供了从最初的软件需求到最后的目标平台代码集成的无缝连接。整个流程基于UML工具与SCADE的桥接，这个桥接很好地平衡了工业标准（UML2，XMI）与DO-178B标准，最终为高安全性项目提供了专有的解决方案。

» 点击获取全文 «

摘自于2006年ERTS

软件开发方法

作者：Sylvain Sauvage, Amar Bouali

摘要

软件设计中的错误越来越成为汽车故障的原因，这一点已成为公认的事实。It is 关于汽车，要考虑的功能模块很多，从车身设计到娱乐系统，从底盘到发动机管理。尽管在许多工程中采用了很好的方法，但是问题仍然出现着。本来容易发现的问题仍能长驱直入，从而引发相关后果。

这种问题的存在使得汽车制造商宁可减少功能的数量，而把工作重心放在了控制复杂性上，从而使得软件与系统更为安全。

用于高安全性领域的软件开发需要对流程，方法与工具进行改进。在本文中，我们探讨运用基于同步语言的软件建模工具的优势。

» 点击获取全文«

摘自于2006年ERTS

将模型驱动设计与不同的形式验证相结合

作者：P. Amey, Bernard Dion

摘要

两种历史上截然不同的技术都给高度集成的软件系统带来强大的工业性能。其中较早的一个是基于语言的静态分析与形式验证，较晚的一个是基于模型的设计与自动代码生成。虽然这两者都效果显著，但都存在问题。幸运的是，这两种方式互相并不排斥，能够较为简单的集成。本文将SPARK与SCADE相结合，用这个例子来说明集成的方式，优势，以及未来存在的机会。

» 点击获取全文 «

摘自于SAE

基于模型开发的形式验证

作者： Amar Bouali, Bernard Dion

摘要

人们越来越多地使用形式验证来检查，确认数字系统的正确性。本文中，我们将介绍对于基于模型的高安全性嵌入式系统的验证，形式验证是一种节约成本的方式。

首先我们介绍形式验证是如何与基于模型的开发方法学相互融合在一起的。在我们所介绍的开发方法学中，整个开发方法是基于一种形式化的语言，是基于正确构造的自动代码生成器。形式验证来证明，你的设计是否满足安全性需求，你运行的代码是否就是最终嵌入的代码。我们将展现运用形式验证的优势，当然开发过程需要遵守IEC 61508 标准，特别是SIL 3与SIL 4这两个等级。我们将详细总结各个形式验证工具在基于模型开发环境中的试用情况。我们集中注意力在安全需求的验证上，包含嵌入式软件的控制逻辑以及数据计算。我们还将解释如何将验证模型的活动与IEC 61508标准中描述的软件生命周期的目标相联系。

我们将用SCADE product以及它的Design Verifier在几个实际汽车项目中得到的数据来说明问题。

»点击获取全文 «

摘自2005年JSAE

在实时嵌入式软件开发中应用形式验证

作者：Amar Bouali, Bernard Dion, Kosuke Konishi

摘要

基于模型的实时嵌入式系统开发使用一种形式化方法进行形式化验证，该方法通过对安全性需求的验证确保了设计的可靠性。形式化验证能够节约成本，省去编写测试用例的时间，通过形式验证，可保证被检查项100％的准确性。另外，基于正确构造的自动代码生成也确保了模型上验证的结果就是对应嵌入式代码的验证结果。经形式化验证的模型可看作从系统需求到软件需求结束的标志。我们说明了基于模型的SCADE开发环境，并讲述了Cruise Control例子。我们还介绍了在软件开发过程中运用形式验证的好处。

» 点击获取全文 «

摘自汽车与交通形式化方法研讨会

在汽车行业软件开发中运用形式验证

注释：本文由大众汽车与奥迪电子提供

形式验证由于其完整性以及能将工作重心前移，因而在汽车行业软件开发中变得越来越重要的。将形式验证融入软件开发过程需要对工具的性能，接口以及支持的语言等方面进行改进。但是在时间触发体系中，还有其他方式来实现工作重心的迁移。本文就将讨论这些问题。

» 点击获取全文«

摘自2004年SAME大会－“2004最佳报告”获得者

使用Esterel语言进行设计与合成

作者：S. Bernardi－德州仪器，S. Lebailly－德州仪器，B. Blanc－爱斯特尔公司，G. Berry－爱斯特尔公司，J. Dormoy－爱斯特尔公司

摘要

这里介绍一种实用的方法来解决多时钟问题，该方法运用了形式化Esterel语言以及它的编程环境。这一方法已经运用于TI的两个设计中，而且这两个设计已经通过集成与验证。

»点击获取全文 «

摘自2004年SAE全球大会

SAE Paper # 4AE-129: 用于高安全性应用软件开发的正确构造方法

作者：Bernard Dion

摘要

在本文中，我们将说明同步方法是如何为高安全系统的正确构造方法提供科学基础的。我们将通过从严格定义的需求到最终的嵌入式代码实现的整个过程来说明这个方法是如何应用于软件设计，验证，实现的。

同步理论已经经过了20多年的理论研究以及十多年的成功工业应用。本文将探讨嵌入式软件三个基本概念：严格的图形文本语言，对于模型的编译算法，形式化验证技术。

最后没，我们将特别说明C编译器是如何正确编译出符合DO-178BA级标准的C代码的(这样省去了代码单元测试)，功能性的测试可以在图形阶段进行，生成的代码是正确的，经过认证的。

»点击获取全文 «

SAE Paper # 2004-01-1768: 通过明确的需求，形式化验证以及正确构造来实现基于模型的开发

作者： Wolfram Hohmann

摘要

本文中，我们将探讨在进入航空电子行业15年后，电传线控已经进入汽车领域。软件已经进入了与安全相关的领域，比如，煞车系统，转向系统，车身动态控制系统。而这些应用也要求嵌入式软件开发过程需要有新的方法出现。

»点击获取全文 «

运用SCADE Suite™有效开发机载软件

作者： Jean-Louis Camus, Bernard Dion

摘要

本文讨论了高安全性航空软件开发过程中成本与生产力问题。按照ED-12/DO-178B 标准进行开发，不仅开发难度大，验证的工作量也巨大。本文首先介绍了传统的开发过程，然后介绍了SCADE Suite方法学及其工具对这一过程的优化。SCADE Suite支持正确构造以及自动生成。它对于开发与验证工作量的节省将详细说明。我们用实例展现了这种方法的效率与优势。

» 点击获取全文 «

同步语言在高安全系统开发中的作用

作者： Gérard Berry

摘要

本文回顾了同步方法以及在关键性嵌入式系统开发中的应用，特别是在航空领域高安全性嵌入式软件中的应用。整个的理念是要从高层需求定义中按照正确构造的方式生成代码。

爱斯特尔技术公司已经将正确构造的理念进行商业化，从而得到了一套高级的开发工具。本文将集中讲述SCADE Suite解决方案. SCADE Suite提供了一套完整的嵌入式模型设计，它有三个强大的技术所支撑：高级的严格意义的图形及文本描述；对于模型的编译方式；形式验证。

»点击获取全文 «

Simulink™ 用户可使用爱斯特尔的SCADE Suite™用以安全性嵌入式软件

Simulink™ 用户可使用爱斯特尔的SCADE Suite™用于安全性嵌入式软件

摘要

航空与汽车系统工程师运用Simulink进行电传线控系统的建模以及控制律验证。来自于爱斯特尔公司的SCADE Suite能使嵌入式开发团队从模型直接生成基于“安全构造”的代码。通过使用SCADE/Simulink桥接器，嵌入式软件开发团队能以最少的时间，最小的代价来确保最终的代码是符合需求的。本文描述了爱斯特尔公司的Simulink Gateway，以及航空与汽车用户是如何使用SCADE Suite来应付开发高安全性软件时面临的挑战。

»点击获取全文 «

从Simulink™经SCADE/Lustre到TTA：分布式嵌入式系统分层解决方案

作者： Paul Caspi, Adrian Curic, Aude Maignan, Christos Sofronis, Stavros Tripakis, Peter Niebert, Thierry Le Sergent

摘要

设计高安全性控制系统需要各级工具间的紧密结合－控制阶段的建模与仿真，软件阶段的开发工具，以及平台阶段的实现工具。当系统是分布式的，平台的选择至关重要，相应的实现工具也要加以选择。如果某个工具箱能够提供各工具间的协同合作，那么就能节约设计与开发的时间，也能增加安全性与成本效应。

在几个欧洲IST项目中，各个工具间的协同合作越来越多地被采用。本文介绍了目前的成果。整个开发都是基于以下三个层次的工具：用于控制算法设计的Simulink，用于软件设计的SCADE/Lustre，以及用于分布式平台的TTA。为什么作出这一选择呢？

» 点击获取全文 «

同步数据流与状态机的保守扩展

作者： JeanLouis Colaço, Bruno Pagano and Marc Pouzet

摘要

本文介绍了同步数据流语言地扩展，例如带有命令语气的Lustre语言在状态机中的应用。这样的扩展是保守的，其含义是程序在扩展后的语言体系中仍保持原意，原来的语法仍旧保留。

从语法的角度，状态机层次上的扩展意味着在每一层包含一组数据流。这种方式是对联合使用Simulink与Stateflow的替代，这种方式结合了两者的特点。

本文的主要内容是通过运用时钟来进行扩展，将祈使结构转化成带时钟信号的数据流结构。用时钟来进行扩展是一种简单的方法，它能在现有的编译器上运行，相应的代码也极具竞争力。这种扩展已经在Scade/Lustre 的ReLuC编译器以及 Lucid同步编译器上实现了。

» 点击获取全文 «

同步数据流编程语言LUSTRE

作者： N. Halbwachs, P. Caspi, P. Raymond, D.Pilaud

摘要

本文介绍了LUSTRE语言，这是一种数据流同步语言，应用于实时系统中－例如自动控制与检测系统，也可用于硬件描述。LUSTRE语言的数据流特性使其与一些领域的描述工具很类似（例如块图，操作符结构，动态采样等等），而它的同步解释能力能很好地处理程序中的时钟问题。再者，这种同步解释能力能使得编译出高效的程序。最后LUSTRE形式化属性很接近于时间逻辑。这些特点使得这门语言可用于编程以及表达某些程序属性，用以验证源程序。

» 点击获取全文 «

实时系统的同步编程

A Tutorial and Commented Bibliography

作者： Nicolas Halbwachs - Verimag

» 点击获取全文 «

运用SCADE对航空电子传感器表决单元进行形式验证

作者: Amar Bouali (Esterel Technologies, Samar Dajani-Brown (Honeywell), and Darren Coffer (Honeywell)

摘要

余度管理已经广泛应用于关键性飞行控制系统中。本文将集中讨论SCADE及其形式验证单元（设计验证器），并以此来评估三余度管理算法的正确性。这个余度管理算法在飞行器嵌入式软件中很有代表性。该算法由Simulink搭建；它有三个传感器输入，一个输出信号以及一个硬件标志位（表明输出的正确性）。本文比较了几种模型验证工具。SCADE在此用以分析表决器的正确性。在应用形式验证工具时，构造一个用于分析表决器是否正常工作的环境是关键一步，本文集中讨论1)构建表决器验证环境的不同方式，2) 不同方法的优势与短处。

»点击获取全文«

对同步语言Esterel进行高层合成

本文介绍了三种用于改善逻辑输入以获取更优结果的技术。

对同步语言Esterel进行高层合成

作者： Stephen Edwards,计算机系, 哥伦比亚大学，纽约

同步数据流语言的基于类型的初始化分析

作者： Jean Louis Colaço (Esterel Technologies) and Marc Pouzet (Laboratoire LIP6)

摘要

同步数据流编程的一大优势是能定义明确的行为。但是运用延迟单元会导致第一拍没有确定的值；所以为了使得数据流编程具有确定性，我们必须使得这些没有明确定义的值不会影响到系统的行为。

本文中进行了初始化的分析，以确保程序行为的确定性。一般来说，这种确定性属性不可确定，本文中做了一个近似，对于大多数数据流程序而言已经足够精确。分析过程是逐位进行的－包括有初始化与没有初始化的表达式－是一个按照子类型限定的类型推理系统。这种分析方法已经在Lucid同步编译器以及新一代Scade-Lustre原型编译器中应用。实际运用中效果良好。