正式方法证明的担忧：理论计算机科学电子笔记中的证据可靠性问题

理论计算机科学电子笔记238（2009）27-39www.elsevier.com/locate/entcs一个用于形式分析正当化的通用的基于目标的证明论证Ibrahim Habli，Tim Kelly易卜拉欣·哈布利，蒂姆·凯利1，2约克大学计算机科学系英国约克摘要形式化方法是在安全关键系统中建立高置信度的强大规范和验证技术。然而，当使用正式方法产生的证据代替传统测试时，对于满足某些认证目标，存在一些担忧。在本文中，我们通过审查DO-178 B和英国国防标准00-56这两个认证文件来解决这个问题，重点是他们接受正式分析证据的方法。 我们还提出了一个通用的基于目标的安全案例，可以实例化，以促进公正和正式分析的认证机构的介绍。安全案例基于以下声明：（1）认证目标的意图，（2）证明形式分析的可信度，（3）在特定项目中部署形式方法的实际可行性关键词：形式化方法，安全案例，安全论证，认证，GSN。1引言形式化方法已经成为一种潜在的技术，用于提高安全关键系统的规范和评估的保证和成本效益。然而，安全标准中的规定阻碍了正式分析技术的采用并使其复杂化。安全关键系统的开发，特别是在航空航天领域，根据严格的认证准则进行监管。在使用之前，有必要根据适用的认证要求对任何新的验证和确认（V & V）分析方法进行评估。 许多标准，特别是DO-178 B指南[2]，认为测试是符合性的首选验证和确认技术1作者要感谢DTI和我们的工业合作伙伴劳斯莱斯公司，捷豹汽车和古德里奇发动机控制系统，支持MOSAIC项目（增量认证的建模、仿真和分析非常感谢Zoe Stephenson的评论本文的格式2电子邮件：Ibrahim.Habli，Tim. cs.york.ac.uk1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.00428I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27在本文中，我们研究了两个不同的认证文件，DO-178 B和英国国防标准00-56[10]，以及每种方法的形式分析。DO-178 B被认为优先考虑测试证据，而国防标准00-56认为分析方法是最强有力的证据。然而，这两个标准，无论其保守性或对正式分析证据的偏好如何，都要求提交关于正式分析为什么以及如何实现认证目标的合理解释。 为此，我们提出了一个通用的安全案例参数，可以实例化，以方便证明和演示的正式分析认证机构。安全案例在英国国防标准00-56中定义为[2]：“A structured argument, supported by a body of evidence that provides a com-pelling,我们提出的安全案例基于以下声明：（1）实现认证目标的意图，（2）证明形式分析的可信性，以及（3）在特定项目中部署形式方法的实际可行性。使用目标结构化符号（GSN）[7]记录安全案例-一种图形论证符号，明确表示任何保证论证的各个元素（要求、声明、证据和上下文）以及这些元素之间存在的关系。本文其余部分的组织如下。第2节和第3节审查了DO-178 B和国防标准00-56中对正式分析证据的考虑。 第4节介绍了安全箱概念。 第5节探讨了 GSN在传达安全案例论证中的作用。在第6节中，我们提出了一个通用的GSN论证，以证明形式分析的合理性。本文最后在第7节中进行了总结2DO-178 B中的形式化分析形式方法的使用在DO-178 B第12节-“附加考虑”中进行了说明。DO-178 B承认形式方法在产生“其操作行为被确信地知道在定义域内的实现”方面的力量它甚至进一步声明，正式的部署等同于彻底的分析，因为它不仅可以检测需求，设计和代码错误，而且还可以消除它们。然而，它随后通过声明形式方法是测试的补充而破坏了上述声明，因此间接暗示形式方法生成的证据不能用作符合验证目标的唯一方法，特别是与可执行目标代码的验证有关的目标。DO-178 B中的高水平处方是使用正式方法获得认证信用的关键障碍，特别是在验证过程中。DO-178 B明确要求执行三个级别的I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）2729基于软件需求的测试生成低水平测试软件集成测试硬件/软件集成测试软件需求覆盖分析软件结构覆盖分析附加验证验证结束直接路径条件路径图1.一、DO-178 B中的测试过程[2]测试1）：低水平测试、软件集成测试和硬件/软件集成测试-而不是“验证”。 正常范围和稳健性测试用例应针对这些测试所解决的每个要求进行开发。所有的测试用例都应该从需求中产生。测试的质量是通过两个覆盖率来衡量的：需求覆盖率和结构覆盖率. 第一种覆盖率决定了哪些需求没有被测试，而第二种覆盖率决定了测试用例对代码结构的执行情况测试是一种强大的验证方法。特别是，由于需要在目标平台上运行软件，测试是软件/硬件集成验证的主导技术。然而，正式的分析技术现在已经得到了很好的建立和证明，可以取代某些应用程序的测试，至少在单元和软件集成级别上对软件进行验证。当前的DO-178 B目标使得使用形式化方法很难获得信任，因为目标对测试非常具体（例如，因为目标被表述为EUROCAE WG 71和RTCA SC205委员会第6小组制定DO-178 C的一个目标是尝试抽象验证目标[9]。如果成功的话，只要能够证明，正式分析将成为一种可能的合规手段 值得信赖并直接针对认证目标。30I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）273英国国防标准00-56英国国防标准00-56第4期[2]采用了不同的安全认证方法。Def Stan 00-56既以证据为基础，又以目标为导向，侧重于安全要求方面证据的强度、严格性和覆盖范围。辩护方Stan 00-56列出了以下可接受的证据类型[2]：a. 分析的直接证据b. 来自演示（测试和/或操作）的直接证据，包括定量证据c. 从审查过程中提取的直接证据d. 过程证据显示开发、维护和操作方面的良好做法e. 良好设计的定性证据，包括专家证词。与DO-178 B不同，测试证据占据了首位，Def Stan 00-56优先考虑分析证据。尽管如此，为了获得使用分析作为主要合规手段的信誉，分析方法应附有支持性的支持资料，包括：合理的解释-说明在特定应用程序中使用分析，包括已知的限制完整的文档-解决分析的配置一致性、可重复性和可验证性工具鉴定-通过自动化和工具支持人员能力-证明在执行分析和使用工具（如可用）模型的适用性-解决模型选择的正确性和合理性，特别是模型代表实际系统某些方面的能力，如时序，资源使用，运行时错误和功能属性。因此，分析证据在Def Stan 00-56中优先，只要它伴随着关于分析方法的可信度和实用性的合理证明。在DO-178 B中，如果向认证机构提供了关于其在满足验证目标方面的有效性的令人信服的论据，则分析证据可被视为一种合规手段-通过测试实现的透明度。这只能在与认证机构达成协议后才能实现。获得这种同意可能会延长获得批准的过程简而言之，在DO-178 B和明确立场00-56，包括提交论据和证据，以证实有关分析方法完整性和有效性的任何声明。 基本上，安全工程师必须提交一份安全案例，以支持I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）2731该制度通过以下规定处理纵深防御原则（P65）：• 危险源与环境之间的多重物理屏障（见第十节）• 一个保护系统，以防止这些障碍的破坏，并减轻障碍被破坏的影响（见第Y节）图二. 一个文本论证的对于与警告相关的危害，继续执行[7]第3.4节中与在未发生设备故障时提供警告的要求相关的假设。特别是，关于第17节中的5.7[4]对于测试操作，需要引入操作限制，以防止危险，同时收集进一步的数据以确定问题的程度。图三.语篇安全论证分析.在接下来的两节中，我们将介绍安全案例的概念，探讨目标结构化符号（GSN）在安全案例论证交流中的作用。4安全性案例论证安全论证通常在现有的安全案例中通过自由文本进行传达。图2显示了使用自由文本传递的安全参数的片段。文本清楚地描述了如何在系统中解释和实现安全要求（P65）。它还清楚地提供了在哪里可以找到支持较低级别陈述的证据的在文本中表达安全论证的结构良好的方法可能是有效的。然而，当文本是表达复杂论点的唯一媒介时，就会遇到一些问题。图3所示的文本摘自一个真实的工业安全案例（识别了隐藏的目标应用程序），说明了其中的一些问题。图3所示的文本不清楚，结构也很差。并不是所有负责生产安全案例的工程师都能写出清晰、结构良好的英语。因此，文本的含义以及安全论证的结构可能是模糊和不清楚的。图3所示类型的交叉引用通常是必要的，因为安全案例的角色是证据的集成者。然而，文本中的多重交叉引用可能会很尴尬，并且会扰乱主要论点的连贯性。32I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27见图4。GSN的主要符号在安全案例中发展、同意和维护安全论证的背景下，使用自由文本的最大问题是确保所有相关利益相关者对论证有相同的理解。如果没有对论点的明确和共同理解，安全案例管理通常是一种缺乏效率和定义不清的活动。 以下部分描述一种结构化技术，用于解决清楚表达和呈现安全论证的问题。5目标结构化符号（GSN）目标结构化符号（GSN）[7] -一种图形论证符号-明确表示任何安全论证的各个元素（要求、声明、证据和背景）以及（可能更重要的是）这些元素之间存在的关系（即具体声明如何支持各个要求，证据如何支持声明以及为论证定义的假设背景）。 表示法的主要符号如下所示 在图4中（每个概念的示例实例当GSN的元素在网络中链接在一起时，它们被描述为“目标结构”。任何目标结构的主要目的是显示目标（关于系统的主张）如何被连续地分解为子目标，直到达到一个点，在这个点上，主张可以通过直接引用可用的证据（解决方案）来支持。作为该分解的一部分，使用GSN还可以明确所采用的论证策略（例如，采用定量或定性方法）、方法的基本原理以及陈述目标的背景（例如，系统范围或假定的操作角色）。图5显示了一个示例目标结构。在这种结构中，和大多数结构一样，存在“顶层”目标-目标结构旨在支持的陈述。在这种情况下，“C/S（控制系统）逻辑无故障”是（单一）顶级目标。在顶层目标之下，结构被分解为子目标，I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）2733S1通过满足所有C/S安全要求进行C1已识别的软件危害S2通过忽略所有已识别软件危害进行G9G5PLC状态机的“Failure1”转换包括BUTTON_IN保持为真非预期的压力机关闭只能由组件故障引起SN1SN3黑盒测试结果SN2C/S状态机事件“由于命令错误，手被困在压力机中”的故障树SN4危害导向测试结果G8非预期打开压机（PoNR后）仅可能是组件失效的结果G7PLC状态机的“Abort”转换包括BUTTON_IN转换G3在压力机通过物理PoNR之前释放控件将导致压力机操作中止G2印刷机控制装置“卡住”将导致印刷机停止G1C/S逻辑无故障图五.目标结构或者直接地，或者像在这种情况下，通过策略间接地。作为解决图5中顶层目标的一种手段，提出了两种论证策略，即这些战略由五个次级目标加以具体化在目标结构的某个阶段，提出一个目标在这种情况下，目标. . 在欧洲，GSN已被越来越多的安全关键行业的公司采用，用于在安全案例中提出安全论点以下列表包括一些应用程序34I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27迄今为止的GSN：• 欧洲战斗机航空电子设备安全鉴定• 鹰式飞机安全鉴定• 英国国防部现场安全司法• 英国多塞特海岸铁路重新信号安全性鉴定• 潜艇推进安全鉴定• 英国军用航空运输管理系统的安全鉴定• 伦敦地铁Jubilee线延长线的安全论证• 瑞典航空运输控制应用。采用GSN的公司所获得的主要好处是，它提高了所有关键项目利益相关者（即系统开发人员、安全工程师、独立评估人员和认证机构）对安全论证的理解。反过来，这提高了利益相关者之间辩论和讨论的质量，并缩短了就所采用的论证方法6形式分析正当化的一般论证与传统的合规性方法（例如测试）不同，正式分析作为主要合规性方法的批准取决于提交令人信服的安全/认证论证，该论证提供证据证明正式技术可以实现并随后实现了某些认证目标。 在本节中，我们将探讨为形式分析提供背景所需的一些基本要素，并记录这些要素在基于GSN的论证中的逻辑依赖关系。形式分析的公正性通常通过与测试的比较来实现认为正式的分析技术这一办法需要开展以下活动：(i) 引出支持标准(ii) 制定一个“至少与“测试论证一样令人信服的论证(iii) 论证实施拟定的分析技术是可行的然而，主要的障碍是提取论证需要满足的认证目标背后的真正意图和理由。例如，DO-178 B文件没有提供指南制定的公开理由。这部分是因为该指南是由I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）2735G2方法{X}符合认证目标C3具体的V V认证目标G7方法{X}具有良好的数学基础C4数学基础G10方法{X}可用C8可用性G8实证案例研究显示了方法{X}A1标准未涉及方法{X}C1适用标准C2一方法{X}S1关于方法{X}的可信度、可行性和认证目标S2关于认证目标的有效性和满足性的S4关于工具支持、可用性和工作人员能力的C7工具鉴定C6C9工作人员能力值得信赖S3关于{X}方法理论可靠性的C5务实诚信C10假设的有效性C11方法{X}已知限制C12模型有效性G3方法{X}值得信赖G11项目工作人员有能力G4方法{X}可实施G1方法{X}可安全实现G9方法{X}使用合格的工具G5确定的认证目标有效G6已确定的认证目标得到满足见图6。新分析技术257家公司和组织，基于行业最佳实践。在本文中，我们通过处理形式分析的证明的三个基本方面来补充上述方法，这三个方面应该被证明论证所涵盖，即：• 引出验证与• 证明形式分析的可信性• 利用现有的项目资源证明采用形式分析的可行性和实用性，例如：工具和人员。上述方面在基于通用GSN的安全论证中实现。图6给出了该参数。论证的顶层目标（G1）是，36I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27⬦--该方法是安全可实现的。其中一个假设是，适用标准（A1）中未明确说明正式分析方法。证明该方法安全性的策略取决于三个子声明：• 该方法符合认证目标（G2）：基于有效性（G5） 和满足（G6）认证目标• 该方法值得信赖（G3）：基于该方法的数学合理性（G7）和实际可靠性（G8）• 该方法是可行的实施（G4）：基于工具的支持（G9），状态能力（G11）和可用性（G10）的方法。次级目标G5、G6、G7、G8、G9和G10下面的符号这种分解取决于每个形式分析方法的具体特征例如，子目标“实证案例研究表明方法X的实际完整性”（G8 ）可以根据从案例研究中获得的实证结果进一步分解，揭示正式方法的优势和局限性。在随后的小节中，我们讨论了可以引出认证目标意图的方法，应该考虑哪些因素来显示形式分析的可信度，以及最终应该证明的项目属性，以显示使用形式分析的实际可行性6.1验证和确认目标为了证实G2 该正式分析涉及认证目标的意图（即，涉及目标的“精神”，而不是实际措辞）。这对于特定于测试的验证目标尤其重要，因为通过正式的分析证据声称满足测试目标可能会出现矛盾。一个更合理的方法是通过形式化分析来声称满足测试目标然而，许多标准，特别是DO-178 B，没有提供制定目标和方法的公开理由。因此，我们建议通过以下方式得出验证与确认目标（尤其是测试目标）(i) 参考已发布的(ii) 根据指南中披露的信息，提出论证，说明证明验证与确认技术的重要性和贡献所涉及的[4]作者或作者的指导原则(iii) 建模和分析认证指南中规定的I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）2737--整个生命周期中不同活动之间的依赖关系上述三种方法是相辅相成的。 例如，DO-178 B不是一份独立的文件相关的指导方针正在不断更新。DO-178 B申请人必须获得认证机构对使用指南的同意。例如，DO-178 B应用的其他指南可以从DO-248 B等技术认证报告中获得[3]。引出测试目标意图的一种补充方法是，仅根据指南和指导中的可用信息，提出支持测试的论据。测试论证的逻辑流程应该显示测试技术与其他先决条件或先决条件技术之间的逻辑相互依赖性。测试技术的输入可能取决于输出数据和其他V V活动的有效性对生命周期过程进行建模和分析，正如标准中所规定的那样，提供了另一种方法来识别测试和其他测试之间的依赖关系。的开发活动，并因此可能推断出推荐或强制测试技术的基本原理。事实上，DO-178 B坚持评估任何替代合规方法对整个开发生命周期过程和数据的影响：“An获得替代方法的认证信用的排序取决于软件级别以及替代方法对软件生命周期过程的影响。6.2关于形式分析图6中的GSN论证中的“方法X是可信的“（G3）声明了形式分析方法的完整性。形式分析的正当性应证明形式分析方法的理论可靠性和实践完整性。例如，如果一个正式的技术解决了浮点运算运行时异常，该技术的可靠性可以证明对二进制浮点运算的IEEE标准（IEEE 754）的要求。一个方法的可靠性也可能因为未能正式地表达某些被认为是由该方法处理的属性（例如功能和时序属性）而受到损害。成功的工业案例研究也很重要，因为它们有可能通过生成经验数据来证明正式分析的有效性。有必要通过案例研究来说明形式化技术如何与其他设计和评估技术相结合。这些案例研究应基于真实的安全关键系统。此外，案例研究应在选定的正式模式的假定真实性的背景下进行。正式分析技术的任何已知局限性也应该被告知，这可能是特定于项目背景的。 例如，证明数学模型和运行时软件行为之间的对应关系是至关重要的[5]。否则，形式分析中的信心将38I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27--被严重破坏。任何形式化的模型都是无用的，甚至可能是误导和危险的，除非它的表示提供了对实际系统的满意的反映。实际的系统包含大量的概念、假设和关系。然而，通常只有一小部分这些元素控制的结构和行为的实际系统。因此，正式模型应侧重于捕捉这些主要因素，以缩小假设系统与实际系统之间的差距。验证模型的真实性无疑是一个普遍的概念，适用于大多数技术，无论它们是否是正式的。然而，这对于形式分析特别重要，因为所得到的分析可能被用作唯一的手段而无需在运行时运行软件。因此，除非能够对正式模型的忠实性达到高度的置信度，否则可能仍然需要进行一些测试6.3形式分析前面的章节阐述了制定令人信服的认证声明的必要性，该声明可以提供强有力的、相关的和充分的证据，证明正式的分析技术满足认证目标。然而，人们总是担心应用正式分析方法的实用性。有一种误解认为，尽管有许多成功的工业实现，但形式化的规范和分析是纯理论的实践[6]。需要向认证机构保证，替代形式分析技术的部署克服了传统上与在大型和关键系统中实施形式方法相关的实际限制，例如[1]，[5]，[6]，[8]：• 工具支撑• 与其他技术的集成性差• 正规数学技能和培训• 保险行业实例• 注重降低成本，而不是提高安全支持另一种形式分析技术的安全案例论证应该反驳关于形式分析的已知误解（G4“方法X是可行的“）。关于实施分析方法的可行性的声明很重要，以表明该方法在分配给项目的资源范围内得到了正确的使用。 例如，上述前三个问题可以 通过开发一种合格的工具来解决，该工具（1）使正式分析过程自动化，（2）与其他开发和验证工具很好地集成。这是必要的工具，以自动化和隐藏的形式，尽可能多的，从而最大限度地减少正式的数学技能的水平，预计将展出的开发人员。I. Habli，T.Kelly/Electronic Notes in Theoretical Computer Science 238（2009）27397份汇总在本文中，我们回顾了两个认证文件，DO-178 B和英国国防标准00-56，重点是他们接受正式分析证据的方法。我们还提出了一个通用的安全案例，可以实例化，以方便正式分析的介绍和证明。 安全案例基于以下声明：（1）实现了认证目标的意图，（2）证明了形式分析的可信性，以及（3）在特定项目中部署形式方法的实际可行性引用[1] 迪尔·D李文，形式化方法的应用，计算机工程学报，2000，第1期（1996）。[2] EUROCAE（欧洲民用航空设备组织），ED-12 B/DO-178 B：机载系统和设备认证中的软件考虑，EUROCAE9（1994）。[3] EUROCAE WG71和RTCA SC205，URL：http://ultra.pr.erau.edu/SCAS。[4] Galloway，A.，R.F. 新泽西州佩奇Tudor，R.A.韦弗岛Toyn和J.A.McDermid，[5] Hall，A.，形式方法的七个神话，IEEE软件档案，第7卷，第5期，汉普顿1（1990）。[6] 霍洛威角H、R.W. Butler，形式化方法在工业应用中的障碍，IEEE Computer1（1996年）。[7] 凯利，T. P.，“论证安全-安全案例管理的系统方法“，博士论文，约克大学，约克，1998年。[8] 骑士JC，C.L. DeJong，M.S.Gibble，L.G.中野，为什么形式化方法没有得到更广泛的，第四届美国宇航局形式化方法研讨会，汉普顿1（1997）。[9] SC-190/EUROCAE WG-52，DO-178 B澄清的最终年度报告：机载系统和设备认证中的软件考虑，EUROCAE9（2001）。[10] 英国国防部，00-56国防系统安全管理要求，英国国防部，第49期（2007年）。