关键软件开发生命周期

理论计算机科学电子笔记243（2009）15-31www.elsevier.com/locate/entcsFoCaL1下关键软件的开发生命周期菲利普·艾罗Etersafe43号，All'eedupontdesbeaunesF-91120 Palaiseauphilippe. etersafe.comThh'er`eseHardin-Semantics，Proofs andImplementation语义学、证明和实现巴黎第6大学信息学104，AvenueduPr′esidentKennedyF-75016 Paristherese.hardin|佛朗哥岛pessaux@lip6.fr摘要在安装之前，关键系统必须由一个独立的权威机构进行评估，该机构确保软件组件真正符合标准中描述的一组要求。这些标准描述了开发过程中必须严格遵循的框架和规则。此外，高度的安全性高度推荐使用正式的方法。在本文中，我们将研究FoCaL开发环境如何帮助满足这些需求并简化评估。该工具旨在帮助关键软件开发的所有阶段，至少在需要正式方法的时候（逐步规范和实现，第一个顺序公式，自动工具帮助的证明）。根据我们作为软件安全评估员或软件工程和形式化方法研究人员的经验，我们通过一个完整的例子提出了一个适应FoCaL规范并符合独立评估要求的开发生命周期。我们展示了继承、后期绑定、重新定义、参数化、封装和声明/定义、属性/定理、由独立证明助手检查的整个开发以及部分自动文档等功能如何用于提高软件组件的全局安全性和重用。关键词：形式化方法，评估，软件生命周期，FoCaL1引言软件开发过程通常表现为两个主要参与者之间的合作：最终用户，其描述了1这项工作得到了国家研究机构ANR-06-SETI-016资助的SSURF项目（安全和安保UndeR Focal）的部分支持。1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.00316P. Ayrault等人/理论计算机科学电子笔记243（2009）15回答“如何”的oper。安全关键软件的开发需要整合第三方参与者，即政府监管机构（当局）。他们的主要任务是在试运行前确认每个开发阶段符合国家和/或国际标准其中大多数标准，如未来用于航空电子设备的DO-178 C2 [2]或用于铁路系统的CENDEEN 50128 [1]，专用于特定领域，而其他一些标准，如IEC-61508[4]或通用安全标准[3]，具有更通用的目的。这些标准通常建立在产品开发周期的经典观点之上，提供了关于要执行的活动、要产生的输出内容、在该周期的每个阶段要执行的验证的要求，并描述了一些强制性的支持活动，如变更和配置管理。对于非关键软件，验证与确认（Veri fication and Validation，V V）是一个相当非正式的过程，通常由软件工程师自己执行。但关键系统无法逃脱第三方专家的全面评估过程。事实上，标准规定了参与开发的不同团队之间的组织独立性水平评估员必须评估从系统级到嵌入式软件的整个开发过程。请注意，由于对系统造成的损害负有法律责任，如果评估员对安全性/安全性/可靠性证明有任何疑问，他/她将拒绝对被评估系统进行调试由于这些原因，关键系统的开发人员最关心的是简化其产品的评估过程，特别是验证生命周期是否符合标准的规定。当必须达到高关键性或保险级别时，标准要求在软件开发周期中使用形式化方法。这些方法通常使用一种无二义性的语言和一些特征来表示和推理属性。它们可以是以证据或核查为基础的，但只有在系统概念、其目的及其潜在危险得到尽可能清楚、准确和完整的描述时，它们才能得到有效-充分的应用。第一作者在通过正式或传统方法开发的关键系统评估方面拥有15年经验，是铁路系统的“第三方”专家。接下来的两位作者致力于FoCaL环境3（本文中介绍）的理论、设计和实现，该环境旨在通过基于证明的形式化方法简化安全关键软件的开发本文的内容来源于评估经验和一些使用FoCaL特性来满足关键系统软件部分开发和评估需求的实验。我们主要集中在本文中的软件生命周期。众所周知，软件生命周期是描述开发团队如何指定，设计，实现，测试和维护软件的一系列步骤每个阶段都由其所需的输入、执行的活动和预期的输出以及文档、所需的属性等来描述。2DO-178 B以一种“柔和”的语气介绍了形式方法3 主页：http://focal.inria.frP. Ayrault等人/理论计算机科学电子笔记243（2009）1517软件周期的不同表示（V-cycle，Waterfall，. . .）.不幸的是，在实践中，有些阶段，如规范或维护，往往没有完全完成。对于关键的嵌入式软件，其周期通常是V周期，主要分为五个（强制性）阶段：需求规范、架构设计、实现和低级别测试、集成/验证测试以及最长的维护阶段。此外，标准要求阶段之间有严格的界限，以及阶段之间的可追溯性，评估过程必须声明这些要求完全达到。每个软件需求都必须与实现它的软件组件以及验证此需求的测试集相关联。类似地，每一行代码都应该与需求（软件需求或架构设计选择）相关联。事实上，许多异常来自从一个阶段到其后继阶段的转换过程中插入的错误，特别是在从规范到设计阶段的过渡通常每个阶段都用一个专门的形式主义来处理，它从一个阶段到另一个阶段都在变化。大多数帮助不同阶段之间的可追溯性的工具都不够强大，无法正式确保在开发下一个阶段时没有插入意外行为。一个可能的解决方案解决这个问题的方法是在整个软件生命周期中使用相同的语言/框架，并根据其形式化能力来选择它，以满足高级别的安全/保密需求。确实存在强大的工具，如J-R Abrial [21]在集合论基础上提出的基于B系统的基于类型理论的FoCaL环境实际上部分受到了B设计师和开发人员的一些工作和讨论的启发而B和FoCaL则有很强的差异性（参见[23]进行比较）。基于我们对B和类型理论的共同知识，以及在B环境中评估软件的第一作者经验，我们在本文中解释了如何在FoCaL中处理软件开发生命周期评估标准所规定的大多数需求使用唯一的形式语言的好处有两个方面：第一，易于跟踪，因为每个阶段的语义表达不需要重复迭代。第二，阶段之间的验证可以通过机械化证明来执行。但困难并没有完全消失。主要的风险是混合和重叠阶段，因此阶段之间的边界模糊。我们记得，只有遵循良好的生命周期开发的软件才能容易地被第三方评估。生命周期的评估还取决于生命周期每个阶段所产生的文件这些人工制品还受到有关内容、可追溯性和维护的标准的严格要求。FoCaL工具提供了一些功能来自动生成软件文档（参见第3节）。我们用一个投票器的开发来说明我们的方法，这是一个遵守纸张大小限制的非常小的例子。然而，安全设备作为这样的表决器被用于安全关键系统中，以防止瞬态故障。18P. Ayrault等人/理论计算机科学电子笔记243（2009）15一些工业项目依赖于正式的方法来构建安全关键系统/软件。通常，开发生命周期以及相关要求是根据所使用的形式化方法的具体特征来处理的。然后，提供论据以说服独立评估人员最终产品的合规性。我们的方法偏离了这些，因为FoCaL本身的发展和所提出的方法深深地嵌入了这些要求。我们通过更好地了解关键开发周期与FoCaL功能之间的关系来获得这种方法的好处论文的其余部分组织如下。我们在第2节中介绍了投票人的文本规范。我们在第3节中概述了FoCaL的主要特征。第4节介绍了安全关键开发的评估需求及其在FoCaL工具中的实例化，编写方式类似于软件质量计划。我们在第5节中详细介绍了投票器的模型化。最后，我们在第6节中总结并提出进一步的工作。2选民概况传感器可能会表现出各种错误，如偏移或设置，比例因子，或瞬态故障，由于对杂散或环境因素（温度，压力，…），即瞬时故障。冗余是用于保护安全关键系统免受这种瞬时故障的主要技术之一。存在多种冗余，这取决于系统应优先考虑哪些特性（安全性、可靠性或两者）。粗略地说，每个冗余组件执行相同的工作，当一个组件出现故障时，其他组件会检测到故障并继续提供服务。通常，投票器用于根据冗余组件例如，表决器用于锅炉中多个传感器的温度采集，或从多个计算机副本中详细说明火车的紧急制动信号。. .投票器的基本原理是根据给定的一致性关系比较其输入值，然后根据预定义的规则输出一个值。投票器中有两个部分• 它的一致性法则，描述了输入值之间的比较策略（严格相等，在一定公差内相等。. .）.• 它的算法，描述了输出值的选择规则（多数投票，错误输入的识别，最严格的投票，最近的值。. .）关键是，在冗余系统中，表决器是必须完美的组件（显然尽可能完美）。投票人的失败被认为是该系统的一个主要弱点。被称为“3选2”（又名2oo3）的冗余参与获得基于连接到多数表决器的3个相同（或功能相同）组件的安全可靠的系统。根据投票结果，系统可以确定要采取的行动（过滤失败，发送警报或系统关闭），以保持在安全条件下。P. Ayrault等人/理论计算机科学电子笔记243（2009）1519在我们的例子中使用的2oo3投票器从三个独立的输入中选择一个值，如果其中至少有两个是一致的。此外，我们还希望检测错误值。因此，第二个输出被添加到voter，以限定第一个结果，如下所示：• 完美匹配：三个输入一致，返回其中一个的索引（例如第一个）。• 部分匹配：三个输入中的两个是一致的，但第三个不是。返回不一致的索引。这使得能够识别此输入上的故障。• 范围匹配：一个输入与其他两个输入一致，而其他两个输入相互不一致。返回一致值的索引。这可能会出现在一致性定律是不传递的（即。在一个宽容的范围内）。在这种情况下，系统可以继续使用最合理的值。• no match：所有的输入都是不一致的，每两个都是。投票人不能作出决定，因为多数规则不适用。没有匹配的情况下的指定，乍一看，似乎是令人满意的：没有值输出，因为没有好的候选者。在规范级别，这种情况是可以接受的，但在设计阶段必须做出选择;连接到表决器的组件正在等待两个值（组件的索引和标记）。根据第二种说法，决定如何处理第一种输出将是它自己的问题。3FoCaL环境FoCaL项目于1998年由T. Hardin和R. Rioboo [7]的目标是在安全框架内帮助关键软件开发的所有阶段，至少在需要或选择正式方法时。这个想法是精心设计一个开发环境，能够为用户提供高层次和另一方面，这个系统必须易于训练有素的工程师使用。目前，FoCaL仍然可以被视为集成开发环境（IDE）的原型，因为语言提供了高级机制，如继承，后期绑定，重新定义，参数化等。这种支持语言被正式描述和研究[6，5，22]。一个FoCaL的发展被组织成一个层次结构，可能有几个根源。层次结构的上层是沿着具体化阶段构建的，而下层对应于实现。层次结构的每个节点对应于朝向完整实现的进展。在这里，我们称细化为建立自上而下的层次结构的过程。FoCaL细化过程已在[6]中进行了正式研究。它与其他精炼概念（如B或TLA）的正式比较仍有待完成。20P. Ayrault等人/理论计算机科学电子笔记243（2009）15物种层次结构中的一个节点称为一个物种。一个物种是一种由字段组成的记录，称为方法，可以是：• 由关键字rep引入的方法，公开了物种值的数据表示。 这种类型称为载体类型。可用类型 大致是：类型变量、ML样类型（具有限制性多态性）和物种携带者类型（即，物种的携带者可以依赖于其他物种的携带者）。此方法是强制性的，可以显式给出或通过继承获得。它可能在某些继承阶段被定义（即只是一个类型变量），但在最终继承分支中必须定义一次且仅定义一次（即只有一次）。收藏）。• 声明，由关键字signature引入，后跟名称和类型（不提供计算主体）。• 由关键字引入的定义由名称、类型和表达式组成。相互递归的定义由letrec引入。 表达式的语法非常接近通常的ML家族语言。• 语句，由关键字属性引入，后跟一个名称和一个用常用连接符（不是和）构建的一阶公式。..）.• 定理，由关键字theorem引入，后面跟着一个名称，一个陈述和一个证明，最终由Coq证明助手检查[14]（见下文）。陈述、定义和证明可以自由地使用该物种的其他方法的名称（由Self！m或更短！m，或者如果作用域中没有名为m的局部函数，则甚至更短的m）。FoCaL编译器（见下文）执行各种分析，以确保属性、定义和证明之间的依赖关系不会导致循环或逻辑不一致。letrec定义不被认为会导致依赖循环。这与大多数常见的面向对象语言有很大的不同，在面向对象语言中，方法被认为是相互递归的，没有任何限制。因此，FoCaL的“对象”模型是不同的，因为物种不是类，也不是面向对象术语中通常意义上的 物种不是第一类价值，只有价值才是活的。满足类型是一个非常重要的问题。在一个类型中，“自我”这个表达方式表示该物种的代表，应该理解为“自我”！众议员物种的元素被称为实体，以强调它们不仅由它们的表示来定义，而且还由操纵它们的功能和它们的属性来定义。继承我们说一个物种A2“改进”了一个物种A1，如果A2继承自A1并“增加了也就是说，在A1中引入的方法和/或A1的载体类型在A2中变得更加具体（更明确）（它不是B的细化概念）。 如果A2乘继承自两个物种Si，P. Ayrault等人/理论计算机科学电子笔记243（2009）1521相同的名字，那么这两个方法的类型必须是兼容的（它们必须有一个最通用的unier[10]）。如果这两个方法都被定义了，那么最后继承的定义（如OCaml[9]）将保留在A2中。此外，A2中可以添加新的方法，并且可以重新定义已经给出的定义。然而，一旦被具体类型完全定义，出于逻辑一致性的原因，rep就接口一个物种的类型是通过消除定义和证据而获得的如果承运人（自！rep）没有定义，它将被认为是一个类型变量（例如，α），物种类型也将被存在绑定器α默默地前缀。这个绑定器将在rep被实例化（定义）后立即被消除，并且必须被消除以获得可运行的代码。一个物种的接口是通过抽象物种类型的所有方法类型中的rep类型获得的，抽象是永久性的（见集合一节）。虽然物种类型对用户来说是完全隐式的，但接口只是由物种名称表示。接口可以通过包含来排序，这一点提供了一个非常简单的子类型概念。收藏一个物种被称为是完全的，如果所有的声明都得到了定义，所有的性质都得到了证明。完成后，一个物种可以提交给其载体的抽象过程，以创建一个集合。 因此，集合的界面是根据其底层物种的类型构建的。因此，集合可以被看作是一种抽象数据类型，只能通过其接口的方法使用，但必须保证所有的方法/定理都被定义/证明，并且用于构建底层物种的不变量不能通过使用这个“架子上的组件”而被破坏参数化种物种可以通过集合来参数化。形参由名称C和接口I引入。 任何具有包含I的接口的集合CC都可以用作C的实际参数。m在物种体（C！rep允许使用C的rep作为抽象类型）。由于任何CC都是从一个完整的物种发出的，因此在运行时不会FoCaL通过参数化允许非常简单的依赖类型：已经引入了集合参数，可以引入表示集合参数载体的值的实体参数。语法禁止参数之间的依赖循环，编译器确保参数之间的一致性后期绑定和重新定义如前所述，方法只能声明。这意味着操作只配备了签名（signature）和属性（property）22P. Ayrault等人/理论计算机科学电子笔记243（2009）15但没有有效的实现。然而，其他方法的定义可能仅指这些声明的方法。 这确实是非常安全的，因为可运行代码只能从集合中获得。 因此，这些只声明的方法将需要在继承层次结构中稍后定义，以便允许构造集合。现在，后期绑定带来了补充的可能性，可以根据它们的最新定义将方法链接在一起。这样，在定义或证明方法m的属性时，可以在任何阶段依赖于尚未实现的方法p，该函数模型足以在m上工作。一旦一个计算体被提供给p，解析机制就会自动链接p和m这种机制还允许在任何继承级别重新定义方法，始终将最新定义的方法保存在从物种中提取的最终集合中。在证明方面，如果m的证明π只使用p的类型，那么当p被定义或重新定义时，π如果需要定义p来证明π，那么很明显，在重新定义p之后，π就不再有效了。编译器根据“旧”定义使所有证明无效，并提示用户重做证明。因此，再定义是完全安全的。校对和自动化由于属性必须被证明，最迟在集合级之前，一个强大的任务是让自动化工具与FoCaL合作，以便让定理证明器自动完成这些证明。FoCaL被设计为对任何类型的证明器开放：它目前支持Zenon[17]，这是由D.多利盖兹[18]。 当Zenon成功时，它产生一个Coq证明项。此外，已经用基于重写的证明器CiMe [15，16]进行了一些实验。这些外部证明器专用于某些特定类型的证明，并可能使开发人员免于手工制作证明。编译今天，对FoCaL源代码的编译导致了OCaml[9]和Coq代码。生成的OCaml代码提供了开发的可执行形式。另一方面，Coq码是由物种源代码、Zenon的证明项和用户直接给出的Coq证明产生的。事实上，得到证明是一件令人满意的事情，但必须确保这些证明确实是正确的。显然，没有人会站在阅读页面的演示来确信这种正确性！Coq代码将由Coq定理证明者进行检查，他将担任评估员，不仅检查开发中包含的所有证明，还检查模型的整体一致性。在可执行方面，目前正在FoCaL团队中执行生成C代码的工作。对大多数编程语言的生成是可能的，因为所需的功能主要是记录数据结构。FoCaL语义最初是在Coq中指定的，这为语言的正确性带来了令人满意的信心另一方面，编译器的校正P. Ayrault等人/理论计算机科学电子笔记243（2009）1523对FoCaL文件安全发展必须包含各种待评估的文件项目。FoCaL可以通过提取可以（并且应该）嵌入开发（代码）和代码本身的注释来帮助创建此文档。如前所述，这些注释可能描述非功能性需求，并可用于可追溯性目的。这些注释在编译过程中被保存，链接到形成软件的FoCaL实体，并且可以由处理程序的抽象语法树的（内部或外部）工具自动处理。FoCaL结合物种的属性和操作（即定理和函数），可以自动生成（在最简单的情况下）描述系统的文档（例如HTML）。此外，UML图可以自动从焦点模型中提取出来.这允许开发人员以图形方式查看其模型，并促进开发人员，客户端和评估员之间的通信4FoCaL中的软件生命周期正如在引言中所说，关键软件的生命周期是基于一个5步的V-周期，类似于经典软件开发周期的V-周期。主要区别在于，在每个阶段之后，由独立验证团队提交可追溯性分析，而另一个独立确认团队执行软件测试。这意味着，当在整个开发过程中使用一种独特的形式时，必须清楚地识别每个生命周期阶段之间的边界如第3节所述，FoCaL模型由用于描述循环所有阶段的物种属性可以表示为一阶公式，这一选择被认为是逻辑框架的表达性和易用性之间的良好折衷事实上，FoCaL不仅适用于计算机研究人员或数学家，也适用于聪明的工程师，最低限度的逻辑背景。目前，FoCaL没有提供语法类别来区分生命周期的不同阶段，我们不确定这种区分对工程师是否有益，因为它们可能会增加太多的严格性。相反，我们建议为开发生命周期的每个阶段提供专用的物种模板。由于每个阶段都处理系统的不同视图，这些模板将由在所考虑的阶段中应该使用（或不使用）的方法（声明，定义，属性，证明）的类型和形式来定义。它们将有助于确定各阶段之间的明确界限，这是核查进程的必要条件。下图描述了软件开发的经典V生命周期。在本文中，我们只考虑需求规范，架构设计，24P. Ayrault等人/理论计算机科学电子笔记243（2009）15Fig. 1. 经典的V生命周期编码和维护阶段。“集成/验证测试”阶段Dubois和M.Carlier [12].4.1质量标准阶段目的是根据客户提供的工作说明书（SOW）指定软件的接口和要求。实际上，需求阶段是一种用软件工程的观点重新表达客户需求的方法。需求通常分为两部分：• 功能需求侧重于描述系统/软件的预期行为，而不涉及任何具体解决方案。这些需求描述了软件的输入和输出之间的关系。• 非功能性需求描述了软件的所有约束，如时间和空间界限，要实现的安全完整性级别，可移植性需求。. .这些需求很难用软件设计模型来表达，但对于发布工业系统来说是强制性的• 对于关键软件，还有第三种需求，称为安全需求。安全性要求来自先前阶段进行的安全性研究的结果。它们确保功能需求永远不会触发Feared Event。它们可以被视为对两个第一种要求。描述质量标准组分的种属将遵循用于质量标准模板的种属。这是一种仅含有以下质量标准要求的种属：• 功能需求由签名（名称和类型）和功能属性（如下所述）表示。• 安全要求也由这些签名上的属性表示。然而，它们的形状与功能属性略有不同，因为它们不表达功能行为的属性，而是功能的特征。• 非功能性的需求不能很容易地用一阶公式来表达，它们被放在注释中，因为它们在编译过程中被保存，所以它们可以得到单独的我们这种技术可以P. Ayrault等人/理论计算机科学电子笔记243（2009）1525签名foo in t_1-> t_2->...->t_n-> Self;（** 企业简介 1 福或 foo。 * ）的文件财产foo_1：所有的i_1在t_1，i_2在t_2，. i_n在t_n中，（*先决条件对的签名. * ）的文件r1（i_1，i_2，...，i_n）->（*后置条件对的签名. * ）的文件r2（i_1，i_2，...，i_n，foo（i_1，i_2，.，i_n））;确保其在整个开发过程中的可追溯性。• 在功能属性保持不变的假设下，证明功能要求符合安全要求• 此外，由于一个组件可以由其他组件参数化，因此必须表达这些其他组件必须遵守的强制属性。我们称之为功能和安全要求都被编码为FoCaL属性。我们通过为功能性的模板引入一个模板来区分它们，如下所示。由于函数属性表示组件的输入和输出之间的关系，因此我们提出以下模板：其中R1和R2是关于签名（本地的或通过参数化导入的）和“粘合”假设的属性在生命周期的这一阶段，可以证明安全要求是由功能的功能要求和对导入功能的胶合假设事实上，FoCaL中的后期绑定和收集机制允许已经执行安全要求的证明，而无需在物种中声明功能的定义，也无需已经完成的来自导入组件的证明。该系统确保在创建定义该系统的集合之前，将给出这些定义并证明其属性。以同样的方式，用户可以确信在生命周期后期作为实际参数传递的组件将完成这些证明，因此他可以在这个阶段安全地假设它们。阶段结束的标准是所有安全要求都得到证明。通常在规范阶段不引入定义然而，一些数学函数的定义可以帮助表达需求：依赖于绝对值函数的定义而不是仅通过其特征属性来表达它更容易我们目前考虑添加一个新的句法范畴（逻辑let）来处理这样的定义的可能性，这些定义在接下来的阶段中可能是无用的（例如，通过绝对值函数的内联4.2架构和设计阶段此阶段专门介绍满足规范要求的体系结构选择。它描述了：• 软件分解成组件，26P. Ayrault等人/理论计算机科学电子笔记243（2009）15• 每个组件的行为，• 组件之间交换的数据，• 组件之间的相互关系（继承，参数化。. . ）的情况下，• 组件的调度对于关键软件，设计应遵循设计规则。这些规则是应用指南，以实现和简化来自支持软件的硬件的所有约束的安全性证明和描述（要执行的内置测试、硬件性能和可靠性）。. . ）或预先存在的软件（操作系统，COTS.. . ）的。根据这一阶段的介绍，我们建议为一个物种设计以下结构：• 软件的分解必须回答两个主要问题：提出有效的租金和尊重前一阶段表达的功能需求。FoCaL• 通过渐进的运营商选择和签名的实现（可能对运营商的结构起作用）来定义行为。FoCaL授权重新定义以前实施的方法此功能可以方便地为载体的特定数据表示专门化算法。• 功能要求的证明确保，通过分解步骤和定义的引入，物种中给出的功能特性确实得到了充分的实现。这实现了阶段之间的可追溯性。规范和设计之间的细化过程可能跨越几个继承步骤。后期绑定允许使用尚未定义的方法，并确保一旦定义，编译器将找到并使用它。这些点对于执行连续和增量细化特别重要。因此，可以增量地实现一些概念，阐明属性，进行证明，并且所有这些都将从父定义中保留（继承），前提是编译器最后一点确保了在任何继承阶段，属性和实现保持一致，即使在重新定义的此外，在一个递增的细化之后，有可能通过遗传从同一个亲本衍生出几个物种。父类可以提供一个方法的默认实现，每个子类可以根据自己的约束自由地重新定义或不重新定义这个实现。显然，工业项目很少从空白页开始。通常重用外部组件（中间件、操作系统原语、COTS）。. .）.出于这个原因，FoCaL提供了一种在模型中使用这些外部组件的方法然而，安全的开发不能一方面简单地假设这些组件是安全的，另一方面不能证明它们的属性，因为这些成本通常是黑匣子。我们的解决方案，在方法论方面，P. Ayrault等人/理论计算机科学电子笔记243（2009）1527是通过测试来验证这些属性是否成立，然后通过发布简化为所承认的关键字的证明来断言这些组件所需的功能属性。这种解决方案肯定是不满意的纯粹主义者，但这是唯一可能的选择时，使用外部COTS。编译器插入这些属性已被文档接受因此，读者会被警告这一点，并可以查看测试结果[12]。像任何开发环境一样，FoCaL提供了一组经过充分验证的“标准”库，开发可以安全地依赖这些库。值得一提的是，有一个多变量多项式的符号计算库，所有基于有序的数学结构和一个通用的访问控制库，大多数常用的访问控制策略都通过它实现了FoCaL迭代软件分解，直到获得所有软件项的证明。软件项目被定义为可以单独编译和测试的最小软件。阶段结束标准是基于软件组件的定义、重用外部组件的属性和“粘合”假设完成功能需求4.3实施阶段这个阶段的目标是生成实现组件的源代码。对于关键软件，应遵循特定的编码规则。这些规则描述了可以使用的语言的安全子集。在此阶段还进行了低水平测试。它允许验证每个软件项目是否符合其文档，并且不包含系统性错误（表在图中，除以零，. .）.在此阶段，软件项是我们建议将以下结构赋予一个物种来实现：• 物种的最后集合。目的是产生一个完整的物种，其中所有的方法都被实现或外部链接（即没有更多的签名没有相关的实现）。• 最后一次集会所引发的证据。它们使用户能够确保在规范阶段设定的一旦获得了这样一个完整的物种，就有可能将其转化为一个集合，这相当于一个有效的软件，能够计算并给出结果。从这个集合中，FoCaL编译器生成软件构建的目标代码。阶段结束的标准显然是当可执行文件被生成时。虽然FoCaL依赖于面向对象的规范和设计，但它不产生面向对象的目标代码。这一点非常重要，因为生成的代码满足标准推荐的安全语言子集，并且独立评估人员可以最后，这允许FoCaL后端到大多数语言，因为它只依赖于共同的和广泛的编程语言功能（主要是模块和记录）。28P. Ayrault等人/理论计算机科学电子笔记243（2009）154.4维持阶段这个阶段致力于保持模型的一致性，尽管有任何要求或强制的演变（硬件过时或更改，增强请求，当局的新法规甚至错误修复）。主要使用的机制是重新定义，继承和后期绑定，只是在定义系统的层次结构中所需的级别。标准要求必须对每一项修改进行跟踪，并明确确定其对整个系统的影响。由于FoCaL提供了非常有效的依赖演算[5]，因此要重做的证明会自动显示，并严格限制在已执行的修改中。由于软件是根据完善的生命周期正式开发的，因此修改的影响受到控制。4.5横突横向过程是在生命周期的每个阶段执行的任务。 设立一个协调发展，有两个横向过程：• 在每个阶段都要进行验证。这些证明有两个目的：所提供的定义的正确性和阶段之间的细化的正确性。最后一点确保了阶段之间的形式可追溯性。• 生成与每个阶段相关的文档。FoCaL模型的证明当然，有些证明不能完全自动化，仍然由工程师负责。然而，经验证明，自动化工具对有效的FoCaL开发有很大的帮助。FoCaLFoCaL与Coq证明助理密切相关[14]，因为它是其最终评估员。Coq是一个已经在工业和学术领域使用的成熟系统[13]，它允许在其验证中投入足够的信心。使用正式的演示检查器作为证明的评估者，避免了手工执行这些验证，特别是防止了这些验证过程中的错误。选择使用Coq显然意味着任何与FoCaL合作的自动证明器必须能够提供Coq证明跟踪作为输出。独特语言的好处在于易于跟踪，因为每个阶段都有独特的语义。图2总结了生命周期阶段使用的FoCaL不要错过开发的文档：在每个阶段，可以从FoCaL模型中提取文档（参见第3节的“文档”段落所有这些文件对于评估人员验证安全问题和测试团队进行确认测试都很有价值。请注意，即使软件是正式开发的，也必须进行独立的验证测试。最后，这个文档可以包含在系统安全案例的工件中。P. Ayrault等人/理论计算机科学电子笔记243（2009）1529（** 规格，规格 物种 福或 THE 埃莱 算法M 部分t.* ）的文件物种Sp_voter（QisSp_qualifierr，SisSp_sensor_index，VisValue）继承Basic_object=（*宣言的的 投票功能：它需要3值和返回一传感器（索引* 限定符）。* ）的文件签名V->V->V->（Si*Q）;签名 传感器rin（Si*Q）->Si;（* GEt 特 第一次试验 组件 外来资产 投票权。 * ）的文件签名 statein（Si*Q）->Q;（* GEt 特 第二节d 组件 外来资产 THE 投票R. * ）的文件（** 功能 要求 一曰： 埃莱 between3 相容的 值s。 * ）的文件财产vote_perfect：所有的v1 v2 v3都是V，（（V！补偿值 （v1，v2）/\V！comp_valuee（v2，v3）/\V！补偿值（v1，v3））->（Si！ equal（sensor（vae（v1，v2，v3）），Si！capt_1）/\Q！ equal（state（e（v1，v2，v3）），Q！））;...（** 约束t on 进口 D 功能： 函数 补偿值MUST Be 对 称 的* ）财产comp_value_is_symmetric：所有v1v2inV，V！补偿值 （v1，v2）->V！int n=nums（nums，nums）;...（*设计相的的选民算法* ）的文件物种Imp_voter（QisSp_qualifierr，QisSp_qualifierr，SisSp_sensor_index，V 价值（Value）继承 Sp_voter（Si，Q，V）=继承参数后期绑定重定义封装Props/proof重用图二. 生命周期中的FoCaL5选民执行情况现在，我们将在开发生命周期之后介绍FoCaL中的投票器的实现。选民指定阶段SpeciesSp voter给出了vote函数的签名、vote的函数要求以及为证明voter而这里，我们强制导入的表示一致性定律的比较函数comp值这避免了考虑所有比较组合的需要。选民设计阶段在这个阶段，我们给出了vote函数的有效实现，并证明它满足功能需求（参见投票完美）。规范Archi/设计编码.维护30P. Ayrault等人/理论计算机科学电子笔记243（2009）15（*定义的的关闭物种* ）的文件种Concrete_coll_int_imp_vote_tol 继承Imp_vote（Coll_etat_vote，Coll_capteur，Coll_int_imp_value_tol） =（*证明的的性能的的进口功能* ）的文件证明的comp_value_is_symmetric =通过Coll_int_imp_value_tol！补偿值对称;...end;;（*最终要点：得到的冷冻和可运行成分 * ）的文件收集Coll_int_imp_vote_tol实现Concrete_coll_int_imp_vote;;int count =unit;（*定义的的载体* ）的文件（*定义的的功能 * ）的文件lete（v1inV，v2inV，v3inV）in（Si*Q）=letc1=V！comp_valueue（v1，v2）inletc2=V ！ comp_valueue（ v1， v3 ）innletc3=V ！ comp_value （ v2 ，v3）inifc1 then如果C2，则ifc3n（Si！ 一号船 长， Q ！perfect_match ）else.（** Proof 外来资产 特 函数要求s.* ）的文件证明的投票_完美=bypropertyySi！comp_transitive，Q！comp_transitivedefinition 投票...选民执行阶段具体的物种是通过向每个投票者的参数提供有效的集合来构建的。在这个阶段，“胶水”假设被证明（c.f. comp值是对称的）。6结论和进一步工作FoCaL是一个活生生的例子，证明可以创建一个学术开发框架，同时集成强大的表达力和语义，有效的目标代码和工业需求来评估所生产的软件。事实上，FoCaL工具在易于开发和标准所施加的约束已经开发了几个例子，如分层自动机的，物理输入采集，本方法。. .在诞生十年后，该语言现在已经足够成熟，可以添加增强功能，并为外部工具带来稳定性和开放性。一个完整的重写的工具，目前执行，以改善编译和促进新功能的整合。其他一些系统范例（如同步功能，高阶参数化，认证的C后端。. . ），并始终牢记所制作的软件在投入使用之前必须由独立机构进行评估。引用[1] “P. Ayrault等人/理论计算机科学电子笔记243（2009）1531[2] “DO-178C/ED 12C，软件考虑在机载系统和设备认证“，RTCA/EUROCAE，出现[3] ”CC，通用标准为信息技术安全信息“，九月 2006http://www.commoncriteriaportal.org/[4] “Functional[5] VirgilePrvosto，“C o n c e p t i o n et Implan t i o n d u lan g e F o C p p e m e n t d e l o gicie l s c e r t i f i s“，Ph D T he s is，P a r i s 6 U i v e r s i y，2003年8月[6] SylvainBoulm'e，[7] Hardin，Th′er′e seanddRioboo，Renaud，[8] Manuel Maarek和Mr.Prevosto，[9] XavierLeroy，JeromeVouillon，DamienDoligezanddother shttp://caml.inria.fr/ocaml/[10] Luis Damas和Robin Milner，第207-212页[11] Robin Milner，[12] M. Carlier和C. Dubois，Berckert和R.Hahnle编辑，LNCS 4966，第84[13] C. ParentBarendregt和T. Nipkow 1994[14] http://coq.inria.fr/“[15] http://cime.lri.fr/“[16] E.作者：J. Forest，O. Pons和X. Urbain，[17] 达米恩多利盖兹，“那Zenon工具“，软件和文档自由可用在http://focal.inria.fr/zenon/[18] Richard Bonichon ， David Delahaye 和 Damien Doligez ， Zenon ： An Extensible Automated TheoremProver Producing Checkable Proofs[19] 今天，让-弗里克·埃蒂恩和韦尔伦在一起，让-弗里克·埃蒂恩和韦尔伦在一起。[20]今天，让-弗里克·埃蒂恩和韦尔伦在一起，让-弗里克·埃蒂恩和韦尔伦在一起。[21] J.R. Abrial，