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