理论计算机科学电子札记108（2004）11-19www.elsevier.com/locate/entcs使用基于形式的工具Constance Heitmeyer康斯坦斯·海特迈耶1，2海军研究实验室（代码5546）华盛顿特区20375摘要在过去的二十年里，形式化方法的研究人员已经产生了许多强大的软件工具，旨在检测错误，并验证硬件设计，软件系统和软件系统工件的属性。过去主要用于调试硬件设计，在未来几年，这些工具应该帮助开发人员提高软件系统的质量。 它们在开发高可靠性软件系统时尤其有用，因为在这些系统中，要求系统具有令人信服的可靠性，以满足关键属性，如安全性和保密性。 本文描述了基于形式化的软件工具在提高软件和软件工件的正确性方面所起的不同作用。这样的工具可以通过自动暴露某些类别的软件错误并通过产生证据（例如，机械检查的证明、执行自动生成的测试用例的结果等）软件系统满足其需求。此外，这些工具还允许从业者将注意力集中在由人执行得最好的开发任务上，例如，获取和验证需求，并构建高质量的需求规范。关键词：形式方法，软件工具，形式规范，形式验证，模型检验，定理证明，SCR。1介绍在过去的十年中，我们在NRL的研究小组已经开发了一个正式的状态机语义和一组正式的工具，以支持SCR（软件成本降低）表格表示法中的需求规范[14，15，16，17]。SCR符号已被许多或-1 作者2电子邮件地址：heitmeyer@itd.nrl.navy.mil1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.11.00412C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）11工业组织开发和分析实际系统的需求规范，包括灯光控制系统，武器系统和空间系统。例如，在2001年，洛克希德·马丁公司使用SCR符号和SCR工具以及测试用例生成器来检测一个关键错误，该错误被描述为我们的目标系统是高保证的软件系统，如航空电子系统、医疗设备的安全关键软件和核电站的控制系统，这些系统需要令人信服的证据来证明系统满足一系列关键属性。这些属性包括• 安全属性（系统防止敏感信息的未经授权的披露和修改、拒绝服务、未经授权的入侵和其他恶意行为），• 安全性能（系统可防止可能导致死亡、受伤、疾病或财产损失的• 容错特性（系统保证一定的服务质量，尽管有故障，如硬件，工作负载或环境异常），• 生存性（系统在攻击、事故或故障的情况下继续完成其任务），以及• 实时特性（系统在指定的时间间隔内提供其输出）。我们小组目前正在研究的两个高可靠性系统是CD，一种在美国使用的加密设备。S. FPE（Fault Protection Engine）是NASA航天器的一个安全关键软件组件CD是基于软件的设备家族的一员，这些设备将为存储在多个不同通道上的数据提供密码学处理，每个通道与不同的主机系统相关联。由于不同通道上的数据可能具有不同的安全分类，因此CD必须强制数据分离，即，确保一个通道上的数据不会与不同通道上的数据冲突，也不会被不同通道上的数据冲突。我们目前正在制定一项计划，正式规定和验证CD软件（使用分离内核[24]来调解对数据的访问）强制执行数据分离。FPE是当前NASA航天器的一个复杂的、安全关键的软件组件，其版本也将用于未来的航天器。FPE的功能是监控航天器软件和硬件的健康状况，并协调和跟踪对检测到的故障的由于FPE的功能对航天器的成功运行至关重要，NASA需要高度保证FPE已被正确实施。为了评估FPE实现的正确性，NRL开发了一个正式的规范-C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）1113FPE最复杂部分的定义和一套测试用例，自动从FPE规范中导出，用于评估FPE软件。使用[9]中描述的算法构建测试用例下面描述的是1）在构建这些和其他高保证软件系统和组件时有用的六类工具这些工具需要改进。此外，开发一个高保证软件系统的一个重要方面进行了讨论，是最低限度地依赖于工具的支持，但大多数工具是有效的必要条件尽管它的重要性，这方面的构造一个高质量的规范所需的行为的系统或软件组件，已在很大程度上被忽视的软件工程研究人员和软件开发人员。2论工具工具可以在获得软件系统满足关键属性的高度信心方面发挥重要作用。下面描述的是工具在提高软件系统和软件系统工件的质量方面可以扮演的六个不同的角色2.1证明格式良好一个格式良好的规范在语法和类型上都是正确的，没有循环依赖，并且是完整的（没有丢失所需的行为）和一致的（规范中没有模糊的行为）。工具，如NRL参考文献[15]和[22]描述了一致性检查器如何发现航空电子系统和轻型制导系统规范中的缺失情况和模糊性。在这两种情况下，检查器都自动检测到了被人工检查所忽略的严重错误。2.2发现财产侵犯在许多情况下，使用工具（如模型检查器）来分析系统规范的某些关键属性会发现违反该属性。给定诊断信息，例如模型检查器返回的反例，开发人员可能会在规范中找到一个规则或一个或多个缺失的或者，属性的公式，而不是规格，可能是不正确的。在所有这些情况下，分析的结果可能是非常有价值的。参考文献[16]如何使用模型检查来检测承包商指定的武器控制系统中的安全属性违规。最近，一些研究人员开始使用模型14C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）11检查以检测软件中的属性违规，而不是软件规范。一个值得注意的例子是Ball和RajamaniSLAM成功使用模型检查来检测严重软件错误的结果导致微软资助开发一种生产质量工具，该工具将使用SLAM中开创的技术来检测设备驱动程序和其他类似程序中的2.3验证关键属性可以使用定理证明器或模型检查器来验证软件工件，例如需求规格说明或设计规格说明，满足关键属性。例如，[21]描述了使用定理证明器来验证CD的早期规范满足一组关键安全属性。2.4质量标准开发人员或领域专家可以使用工具，如模拟器或动画师，来检查正式规范是否捕获了预期的系统行为。通过模拟器运行场景，用户可以确保系统规范既不会遗漏也不会错误地指定系统要求。例如，在开发FPE规范时，仿真不仅在调试规范方面非常有价值，而且在从领域专家那里获得关于所需行为的反馈以及向项目发起人演示FPE规范捕获的行为方面也非常有用。2.5构造测试用例从一个形式化的规范中，测试用例生成器可以自动生成一套满足某些覆盖标准的测试用例，例如分支覆盖[9]。在以SCR或RSML（需求状态机语言）[12]（一种受状态图启发的需求语言）表示的规范中，规范中每个因变量的值由总函数定义。在分支覆盖中，每个部分（即，分支）构成了构建测试用例的基础。总之，以这种方式构建的测试用例集“覆盖”了每个条件（即，分公司）在规格。在FPE项目以及其他涉及高保证系统的项目中，自动化测试用例生成对软件开发人员来说非常重要，因为1）自动构造测试的成本比手动构造测试的成本低得多C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）11152）一组“覆盖”规格的测试用例2.6检测编码错误和代码漏洞静态分析工具可以在不执行软件的情况下对软件进行分析，这种工具可以自动检测源代码和汇编代码中的错误和漏洞，如未初始化的变量、错误的指针、算术运算和编译器。帮助检测C代码中此类错误的工具的示例包括Codesurfer [6]和Safer C，它们可以发现代码中的危险漏洞，例如[11]中描述的漏洞。Bishop等人描述了静态分析工具如何帮助发现许多安全关键系统中使用的COTS软件中的漏洞[4]。3需要改进的尽管工具在调试和产生软件和软件工件的正确性的证据方面非常有用，但是迫切需要许多工具改进。这些改进，其中一些以前在[13]中建议，如下所述。3.1自动抽象在实际的软件规范可以有效地进行模型检查之前，必须解决状态爆炸问题，即，必须减小要分析的状态空间的大小。 减少状态爆炸的一个有效方法是应用抽象。 例如，对武器控制系统的大规格进行模型检查[16]直到应用了两种抽象才成功。不幸的是，最常见的方法是以特别的方式开发抽象-抽象和原始规范之间的对应关系是基于非正式的，直观的论点。 需要的是可以自动构造的数学上合理的抽象。在自动构建声音抽象方面的最新进展已在[3，16]中报道。3.2可理解的反馈当形式分析暴露出错误时，应该向用户提供易于理解的反馈，这些反馈有助于纠正错误。已经存在用于在一致性检查中实现这一点的技术（参见，例如，[18]）。虽然16C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）11由模型检查器产生的反例通常提供有用的诊断信息，但它们有时很难理解。一种很有前途的方法是使用模拟器或动画师来演示和验证反例。3.3自动生成的不变量需要一些工具，比如[19]中描述的工具，可以从一个规范自动构造不变量。已知的不变量在软件开发中有许多用途。它们可以作为辅助引理用于证明软件规范的定理。例如，关于早期CD规范[21]的一些需要证明的安全属性在没有辅助不变量的情况下无法证明。这些不变量是使用[19，20]中描述的算法自动生成的。 不变量还可以用于验证需求规格说明-领域专家可以使用自动生成的不变量来确定规格说明是否正确地捕获了某些所需的系统行为。3.4更多虽然机械定理证明器已经被研究人员用来验证各种算法和协议，但它们很少用于实际的软件开发。为了更广泛地使用证明器，需要克服一些障碍首先，证明器提供的规范语言必须更自然。第二，证明者支持的推理步骤应该更接近手工证明中产生的步骤;当前的证明者支持的推理步骤太低，而且太详细。这个问题的一个部分解决方案是构建一个prover前端，旨在支持一类特殊数学模型的规范和证明这样的前端的一个例子是TAME，PVS的一个虽然使用机械证明器仍然需要数学成熟度和定理证明技能，但使证明器更加“自然”和方便使用应该会鼓励更广泛的4有效使用工具还需要什么虽然研究人员（和许多软件开发人员）通常会花费大量的精力来应用工具，但他们通常很少花费精力，也很少关注创建高质量的系统规范。因此，许多当前规范难以理解和更改，而且组织也很差。迫切需要的是更高质量的要求规范，C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）1117软件设计该等规范至关重要，因为其可作为客户、开发人员、验证团队及其他持份者之间进行精确沟通的媒介。提高规范质量的一种方法是选择一种“好”的这种语言必须是“自然的”;在可行的范围内，应该支持软件从业者熟悉的语言语法和语义。语言还必须具有明确定义的形式语义，并且应该可伸缩。此外，应该向从业者提供用语言表达的经过深思熟虑的示例规范。通过研究这些例子，从业者可以学习如何使用这种语言来创建既简洁又易于理解的我们的小组和其他人（见，例如，[7，5]）已经成功地应用SCR表格表示法来表达许多软件系统和软件组件所需的行为。SCR规范的确切含义由[15]中描述的状态机语义给出。其他人，如Heimdahl和Leveson[12]，提出了一种结合表格和图形的混合符号。基于表的规范语言有很多优点。表格规范不仅易于理解，而且对于软件从业者来说（相对）容易构建，此外，表格为从业者之间的沟通提供了精确，明确的基础。它们还提供了一个自然的组织，允许独立的建设，审查，修改和分析一个大规格的小部分。最后，表格符号的规模。表格规格的可扩展性的证据在20世纪90年代早期得到了证明，当时洛克希德公司的工程师使用一组表格来规范C-130 J飞行计划的完整要求，该计划包含超过25万行Ada代码。除了表格符号外，还应探索其他用户友好的符号。例如，许多研究人员和从业者使用表示为消息序列图（MSC）的场景来捕获系统需求，MSC是通常用于描述通信协议的符号。由MSC表示的需求可以直接分析（参见，例如，[23]）或转换为另一种表示进行分析，如[26]。即使选择了一种好的规范语言，高质量的规范仍然需要规范者的高度关注和技能。建立一个好的规范有点类似于设计一个好的证明。就像一个好的证明一样，这样的规范应该很容易理解。 在大多数情况下，它还应该没有冗余，尽管一些计划的冗余是可以接受的（例如，关键系统属性的列表）。减少冗余产生更简洁的规范，这是规范18C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）11复杂的大型系统。此外，规范应仔细组织，以便于理解和易于更改。最后，一个好的规范应该是一个参考文件，这样规范中的信息就很容易找到。5结论工具在构建高可靠性软件系统时非常有用。它们可以发现人工检查遗漏的错误，帮助验证规范，为验证属性提供机械化支持，减少构建（和执行）一组测试用例所需的时间和时间，并通过基于某些覆盖标准构建一套测试用例来提供测试结果的更多信心。因此，一组强大的工具可以解放人们去做生产高质量、高保证的软件系统所需的艰苦的智力工作。这种智力资源的一部分应该用于获取系统和软件需求的知识，并用于生成易于理解、组织良好的需求规范。引用[1] Archer，M，TAME：Using PVS strategies for special-purpose theorem providing，Annalsof Mathematics and Arti ficial Intelligence29（2000），139[2] 球，T。和S.K. Rajamani，SLAM项目：通过静态分析实现系统软件，Proceedings，29 th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages（POPL 2002），ACM SIGPLANNotices 37，Portland，OR，ACM Press（2002），1-3。[3] Bensalem ， S. ， Y. Lakhnech 和 S.Owre ， Computing abstractions of infinite statesystemscompositionally and automatically，Proceedings，Computer-Aided Verification，10th AnnualConference （ CAV '98 ） ， Vancouver ， B.C. ， Canada ， June 28 - July 2 ，1998，LNCS1427（1998），319-331.[4] Bishop，P.，R. Bloom field，T. Clement，S. Guerra和C. Jones，COTS/SOUP的完整性静态分析，会议记录，第22届计算机安全、可靠性和安全国际会议（SAFECOMP 2003），爱丁堡，英国，9月。23-26，2003，LNCS2788（2003），63-76.[5] 布莱克本M.，R. Knickerbocker和R.林文雄，应用自动机架构于火星登陆器着陆监测器，会议论文集，洛克希德马丁公司联合研讨会（2001年）。[6] Codesurfer用户指南和技术参考，版本1.0，Grammatech（1999）。[7] Faulk，S.R.，J. Brackett，P. Ward和J. Kirby，Jr.，实时要求的核心方法，IEEE软件9（1992），22[8] Feather，MS，S. Fickas和N. A.李文，“故障保护系统的模型检验”，第六届高可靠性系统工程国际研讨会论文集（HASE 2001），IEEE计算机学会（2001），32[9] Gargantini，A.和C. Heitmeyer，Using model checking to generate tests from requirementsspecifications，Proceedings，ACM 7th European Software Engineering Conference/7th ACMSIGSOFT Symposium on Foundations of Software Engineering ， 2009 年 9 月 。1999 ，Toulouse，FR，LNCS1687（1999），146C. Heitmeyer/Electronic Notes in Theoretical Computer Science 108（2004）1119[10] Harel，D.，Statecharts：A visual formalism for complex systems，Science of ComputerProgramming8（1987），231[11] 哈顿湖“更安全的C：为高完整性和安全关键系统开发软件”，McGraw-Hill，纽约，N。是的，一九九五年[12] 海姆达尔，M. P. E.和N. G.李文生，层次化需求的完备性与一致性，国立成功大学资讯工程研究所硕士论文，（1996）[13] Heitmeyer，C.，关于实用形式化方法的必要性，会议录，实时和容错系统的形式化技术，第五届国际研讨会，林比，丹麦，9月。1998，LNCS1486（1998），18[14] 海特迈耶角L.，软件成本降低，软件工程百科全书，J.J.Marciniak编辑，第2版，约翰威利父子公司，New York，N.Y. （2002），1374[15] Heitmeyer，C.L.，R. D. Je Escherords和B. G. Labaw，Automated consistency checking ofrequirements specifications，ACM Transactions on Software Engineering and Methodology5（1996），231[16] Heitmeyer，C.，小J·柯比B. Labaw，M. Archer和R. Bharadwaj，Using abstraction and modelchecking to detect safety violations in requirements specifications，IEEE Transactions onSoftware Engineering24（1998），927[17] Heitmeyer，C.，小J·柯比B. Labaw和R. Bharadwaj，SCR*：用于指定和分析软件需求的工具集，会议录，计算机辅助验证，第10届年度会议（CAV '98），温哥华，不列颠哥伦比亚省，Canada，June 28 - July 2，1998，LNCS1427（1998），526-531.[18] Heitmeyer，C.，小J·柯比和B. Labaw，用于正式规范、验证和确认需求的工具，会议记录，第12届计算机保证年会（COMPASS[19] 杰 奥 尔 德 斯 河 D. 和 C.L. Heitmeyer ， Automatic generation of state invariants fromrequirements specifications，Proceedings，Sixth ACM SIGSOFT International Symposium onFoundations of Software Engineering，Nov. 3-5，1998，Lake Buena Vista，FL（1998），56[20] Je Escherords ， R. D. 和C.L. Heitmeyer ，An algorithm for strengthening state invariantsgenerated from requirements specifications ， Proceedings ， Fifth IEEE InternationalSymposium on Requirements Engineering（RE 2001），2001年8月27-31日，多伦多，加拿大（2001），182[21] Kirby，J.，M. Archer和C.Heitmeyer，SCR：构建高保证COMSEC系统的实用方法，会议记录，第15届计算机安全应用年会，IEEE计算机协会（1999年），109[22] 米勒，S。P.的人，在Core和SCR中验证轻型制导系统的模式逻辑，Proceedings，2nd Workshopon Formal Methods in Software Practice（FMSP[23] Peled，D.，信息序列图工具集，计算机辅助验证会议录，第10届年会（CAV '98），温哥华，不列颠哥伦比亚省，Canada，June 28 - July 2，1998，LNCS1427（1998），532[24] 拉什比，J.M.，安全系统的设计和验证，Proceedings，第八届操作系统原理研讨会，1981年12月14-16日，Paci fic Grove，CA，Operating System Review 15（1981），12-21。[25] Shankar ， N. ， S. Owre 和 J.Rushby ， PVS 证明 ：参考 手册， 计算机科 学实验 室， SRIInternational，Menlo Park，CA（1993）。[26] Uchitel，S.，R. Chatley，J. Kramer，and J. Magee. LTSA-MSC：使用隐含场景的行为模型评估工具支持，会议记录，第九届系统构建和分析工具和算法国际会议（TACAS），华沙，2003年4月。
我的内容管理
展开
