为关键任务应急柴油发电机验证高完整性控制软件

在主电源中断的情况下，发电厂运营商依靠柴油发动机驱动的发电机作为处理重要功能所需的备用电源。核电站的应用要求最高的安全性和可靠性标准。MTU发电机组符合这些标准。

为了确保发电机的可用性，MTU柴油发动机(图1)使用高完整性控制软件。本软件的开发基于IEC 60880标准。IEC 60880定义了用于基于计算机的仪器仪表和核电站控制系统的软件的要求，特别是执行IEC 61226定义的安全类别A功能的软件。每个国家的核管理机构可以补充这些要求，每个机构对控制软件及其开发过程进行独立审计。

MTU已经建立了一个专门满足IEC 60880要求的结构化开发流程。这个工作流的一个关键部分是Polyspace的使用^®代码验证器，用于识别和消除下溢、溢出、除零、内存访问和其他运行时错误。Polyspace代码验证器突出显示被证明没有某些类型的运行时错误的代码，使团队能够将审查重点放在剩余的代码上。

标准开发过程的缺点

当我们开始开发控制软件时，我们在IEC 60880要求方面的内部专业知识相对较少。我们最初的策略是使用我们的标准商业软件开发过程，同时生成更多的文档并进行额外的测试——包括对一些遗留代码的运行时错误进行Polyspace测试。

Polyspace代码验证器将代码中的每个元素高亮显示为绿色、红色、灰色或橙色，以指示其状态。在我们的代码中，有几行被标记为红色，这意味着它们被证明是错误的(但被证明是正确有效的语句)。大量的元素被显示为绿色，表明它们没有运行时错误;然而，一些橙色或未经验证的元素也被突出显示。详细的结果使我们更容易识别代码中的问题，并证明未经验证或无法到达的代码。然而，即使是最详细的结果也不足以证明监管机构和我们的客户的软件满足标准的要求。我们还必须表明，用于获得结果的过程和工具是值得信赖的。

我们必须建立一个新的、高度复杂的开发流程，使我们能够满足IEC 60880的要求。代理机构和客户需要证明我们有一个软件开发计划，我们使用的工具是合格的，我们遵循了计划并正确地使用了工具。

合格的Polyspace代码验证器

我们新的软件开发过程的一个关键元素是工具链管理，这一领域涉及软件开发和测试工具的选择和鉴定。IEC 60880第14章涵盖了软件工具的适当使用，包括那些可以增加软件开发过程完整性和提高软件可靠性的工具。工具的定义是任意一种至关重要的或被．文字处理器就是一个非关键工具的例子。关键工具是可能会在软件中引入错误的工具(例如，编译器)，或者可能导致软件中遗漏错误的工具(例如，验证工具，如Polyspace Client)™对于C / c++)。

在我们使用高完整性软件开发的关键工具之前，我们必须确保它适合于任务，并且能够正确地运行。为了验证Polyspace代码验证器和其他关键工具，我们创建了包含详细验证计划的单独工具验证文件。该计划包括三个核心领域:正确的工具功能、结构化的工具开发和工具使用的直接体验。

对于第一个领域，正确的工具功能，我们使用了测试用例、过程、预期结果，以及来自DO qualification Kit和IEC Certification Kit的其他鉴定工件(图2)。对于第二个领域，我们还回顾了认证机构TÜV SÜD对用于创建多空间代码验证器的结构化开发过程的评估。对于第三个领域，我们记录了我们自己对Polyspace代码验证器的使用，并将其与额外的Polyspace产品使用信息结合起来，这样我们就可以根据我们自己的用例调整认证工具包。

总的来说，我们有超过10个单独的Polyspace认证措施，所有措施都没有偏差地通过，使我们能够向客户和监管机构证明，我们的工具策略和过程足以验证Polyspace客户端用于C/ c++和Polyspace服务器™用于C/ c++作为验证工具。

日常开发中的Polyspace代码验证

在开发柴油发动机控制软件时，MTU开发人员使用Polyspace代码验证器在将代码检入版本控制系统之前检查其运行时错误。这种级别的非正式测试为开发人员的代码提供了即时反馈，使他们能够在正式的集成测试之前解决任何突出的问题。MTU构建工程师还运行Polyspace代码验证器，作为自动化夜间构建和测试过程的一部分，使用结果确定需要更多开发人员关注的代码区域。

开发人员不允许提交带有已知运行时错误(红色突出显示)的代码，但是他们可以提交带有未经验证(橙色)或不可到达(灰色)元素的代码。然而，每一个因素都必须被证明是合理的，这意味着解释为什么这不是一个问题。例如，作为一种防御性编程实践，开发人员实现了每一个开关用C语句加上a默认的正常操作无法达到的选项。这些默认的选项正确地用灰色突出显示。每个实例都被认为是合理的，因为我们确切地知道是什么原因导致Polyspace代码验证器将其标记为不可访问的代码。

Polyspace代码验证器提供了对解释为什么标记为橙色的每个代码元素都被视为未经验证的信息的访问。例如，它们可能突出显示绝对内存地址的使用，这些地址有时在嵌入式软件中是硬编码的。在其他情况下，他们可能会注意到操作可能导致溢流或下溢情况。然后，开发团队负责证明这种潜在的失败条件或根据需要纠正代码。

形式验证

在将所有代码集成到版本控制系统之后，我们运行Polyspace代码验证器来重新检查整个代码库。一个正式的评审团队检查并证明标记为红色、橙色或灰色的每个代码元素是正确的。嵌入式控制软件通常包含无限循环。Polyspace产下载188bet金宝搏品正确地将这些循环识别为非终止，但没有其他代码为红色。

因为这是我们第一次在IEC 60880管理的项目中使用Polyspace产品，所以我们很早就决定在Polys下载188bet金宝搏pace验证的同时进行人工审查。这种手动检查需要大量的工作，并且没有发现任何额外的问题。手动审查的一个主要缺点是它们依赖于人工审查人员，因此不可重复。相比之下，Polyspace代码验证器无论在同一代码上运行多少次，都能提供一致的结果。当我们修复了一个问题时，我们可以看到它已经被解决了，因为对应的代码是绿色的，我们可以确保我们没有不经意地引入新的问题。

扩展Polyspace代码验证的使用

随着柴油发动机控制软件在审批过程的最后阶段，MTU工程师已经开始在其他项目上使用Polyspace代码验证器，包括几个使用基于模型设计的商业非安全控制软件系统。在这些项目中，我们首先用Simulink对系统建模金宝app^®和Stateflow^®然后使用嵌入式编码器生成C代码™．我们使用Polyspace产品来验下载188bet金宝搏证生成的代码。在源代码中识别的每个问题都链接回Simulink模型，使我们能够追踪潜在问题的根源。金宝app