ACM通信

软件工程社区设计了许多技术、工具和方法，旨在提高软件的可靠性和可靠性。这些方法都取得了不同程度的成功，有些方法在特定领域或特定类别的应用程序中取得了比其他方法更好的结果。一种流行的，尽管不是没有争议的方法被称为正式的方法其中，一种具有形式化语义的规范符号，以及用于推理的演绎装置，被用来指定、设计、分析并最终实现硬件或软件(或混合)系统。

这种方法通常被认为是很难应用的，需要大量的数学经验。^1，1111经验表明，没有显著数学能力的开发人员至少可以理解和使用正式规范，即使更强的数学能力和专业化在数学和工程的各个领域都需要更具有挑战性的形式化方法相关的活动，如验证和改进，甚至编写形式化规范本身的任务。随着自动化形式化方法逐渐成为设计过程的自然组成部分，作为软件产品的标准特征，我们也体验到了更高的可靠性级别。

然而，一个关键的问题是，那些应用形式化方法的人需要能够在适当的表示级别上抽象和建模系统，也就是说，开发可靠的设计原则并将它们应用到软件开发中。在验证更复杂的系统的属性时尤其如此，这些系统涉及到组件之间的显著并发性和交互。当我们想证明性质时，通常更容易也更有必要在更抽象的层面上证明它们，利用的概念抽象的解释。

本文包含了三位在软件工程、抽象解释和并发系统验证领域享誉世界的专家的贡献:Michael A. Jackson、Patrick Cousot和Byron Cook。他们的贡献是基于他们在2007年9月1014日在伦敦举行的IEEE第五届软件工程和形式化方法国际会议上的主题演讲。该系列会议的目的是将形式化方法和软件工程领域的从业者和研究人员聚集在一起，目的是开发协同作用并进一步加深我们对专门化、抽象和验证技术以及其他领域的理解。

回到顶部

可靠性水平下降

基于计算机的系统无处不在，现在几乎影响了我们生活的方方面面。它们在早上叫醒我们，控制我们的食物烹饪，以媒体播放器的形式招待我们，帮助避免交通拥堵，控制或识别(通过GPS导航系统)我们乘坐的车辆的位置，洗我们的衣服，甚至从我们的银行账户中给我们现金(有时!)

计算机正被越来越多地用于对我们的生存产生巨大影响的应用领域。²他们控制着地铁里的列车流量，铁路线路上的信号，甚至是街道上的红绿灯。这些系统的任何故障都可能造成极大的不便，并可能导致生命损失的事故。由于它们控制着飞机的实际飞行，化工厂的冷却系统，核电站的反馈回路，等等，我们可以看到，如果它们不能按预期运行，它们都有可能造成巨大的灾难。

这些系统越来越多软件密集型这意味着软件是主要组件，大部分功能是通过软件而不是硬件实现实现的。这就提出了问题可靠性(衡量系统在一段时间内持续运行的能力¹²)和可靠性(可以合理地依赖于它所提供的服务的属性¹²)的软件。

回到顶部

软件危机

这已经成为软件工程社区的一个主要问题。虽然硬件可靠性多年来不断提高，而且最可靠系统的平均故障时间(可靠性的衡量标准)现在超过了100年，¹³软件并没有跟上这种模式，实际上已经显示出可靠性水平的下降。¹⁰

这可以归因于许多因素，包括:

• 一个naïve的信念:任何会写软件的人都能写好软件
• 一个错误的信念，运行一些代表性的测试用例表明软件是“正确的”或充分的。
• 不明白实现是件好事设计比产生大量的代码更重要，软件工程的目标不仅是产生代码，而且是对问题产生可靠的解决方案，这些解决方案最终可以用编程语言实现。
• 未能意识到对软件的更改，特别是不必要的、不受控制的和粗心的更改，可能会影响其适当性和有效性，影响其正确操作，并可能使其效率降低，甚至在极端情况下过时。

当然，软件是目的要改变，就必须能够改变。如果我们编写的软件在部署后永远不会更改(以满足不断变化的需求、不断发展的环境，或纠正错误、未实现或不正确实现的需求)，那么我们最好在硬件中实现一切;但这在技术上是不可能的，在财务和空间上也是不可行的。

回到顶部

迈克尔·杰克逊:专攻软件工程

软件密集型系统旨在与人类和物理问题世界进行可靠的交互。软件的执行产生并使用关于世界的实时信息，并监视和部分控制其行为，以提供所需的功能并满足所需的约束。

这种系统提出了一个特殊的挑战，来自于软件的准正式性质和计算机之外的人类和物理问题世界的非正式性质之间的相互作用。正在执行的软件可以被视为一个正式的系统:除了最极端关键的系统外，所有的计算机行为都可以假定符合程序语义。相比之下，非正式问题世界有许多部分——人类的、自然的和工程的，它们的性质和行为远没有那么可靠。对于一个可靠的系统，必须有一个足够的问题世界的正式模型，并且软件必须被设计成反映这个世界符合这个模型的假设。在执行它的程序时，计算机总是表现得好像世界模型是有效的;如果世界偏离了这个模式，这个系统就会以某种方式失败。问题世界是非形式的，具有无限可能的行为和属性，可以使任何形式模型失效。在适当选择的方面削弱模型的容错技术可以减轻困难，但不能消除它:世界仍然可以使削弱的模型无效。那么，如何设计一个可靠的系统呢?

首先，正式模型的开发是一项工程任务。在已建立的工程分支中，挑战是通过在每个特定产品类别中积累的经验来解决的正常的设计原则。航空工程师w·g·文森蒂(W. G. Vincenti)解释了正常的设计:“工程师一开始就知道该装置是如何工作的，它的习惯特征是什么，如果按照这些原则进行适当的设计，它就有很大可能完成预期的任务。”例如，家用汽车是全行业常规设计原则的产物。不同制造商的产品无论在外观上还是在内部工作方式上都惊人地相似，因为他们的设计师都严格遵循当前的正常设计。这种正常的设计体现了对模型的积累知识，包括产品本身和它的环境或问题世界，这些知识足以满足所需的可靠性水平:模型中的哪些偏差是不太可能被忽略的;由普通设计配置隐式处理;在正常设计实践规定的计算和检查中必须明确考虑到这一点。

缺乏可应用的正规设计学科的工程师必然要从事激进的设计。用文森特的话来说:“在激进的设计中，设备应该如何布置，甚至如何工作在很大程度上都是未知的。设计师以前从未见过这样的设备，也没有成功的假设。问题是要设计出足够好用的东西来保证进一步的开发。”简而言之，激进设计对可靠性的期望很低:只有在纯粹的实验工作中，或者在新奇和刺激是最重要的、可靠性不被重视的地方，它才可能是一个不错的选择。

一个正常的设计原则不是轻易或偶然产生的。它依赖于一种文化专业化它是一个由组织和个人组成的社区，致力于一个特定产品类别的正常设计及其所体现的科学和工程知识的逐步、长期发展。这种专业化文化的先决条件有两个:专业团体的继续存在，以及它们的研究和生产设施以及它们的期刊和会议;以及每一代极具天赋的工程师都希望将他们的职业生涯只专注于一个专业领域。这种专业社区的基础设施和发展一个成功的正常设计学科所需的进步是流动的通才群体无法实现或持续的。

软件工程和计算机科学已经有许多专业:一些在复杂性理论、并发性、实时系统、编程语言、模型检验、程序证明和分布式计算;以及一些系统软件组件，如编译器、数据库系统、病毒检查程序和SAT(布尔满足性问题)求解器。然而，这些专门化是不够的。为了构建可靠的软件密集型系统，我们必须模仿已建立的工程分支，开发更多的专门技术，这些专门技术非常专注于终端产品的窄类及其组件子系统。只有面向产品的专家才能通过汇集设计任务的所有不同方面、部分和维度的专家的贡献来实现可靠性。

那么，需要哪些特定的专门化呢?我们无法提前回答这个问题，也无法用任何系统的、权威的方式回答这个问题。在一个坚持可靠系统的社会中，在一个重视并激励专门化的软件工程文化中，特定的专门化将会随着它们被认识到的机会和挑战而出现和发展。

总之，工程产品的可靠性必须基于正常的设计规程。只有在以产品为导向的常规设计学科中，才能将所有必要的知识隐性和显性地聚集在一起，以建立一个可靠的系统。这个正常的学科反过来必须是专门研究特定产品类别系统的工程师长期社区的产物。对于一个关键的软件密集型系统，专业化是不可选的。

回到顶部

帕特里克·库索:抽象解释在形式方法中的作用

形式验证方法。在计算机科学和软件工程中，正式的方法是基于数学的技术，用于软件和硬件系统的规范、开发和验证。它们建立所需属性的满足(称为规范)通过一个正式的模型(称为语义)系统的行为(例如，程序及其物理环境)。的语义域是所有系统行为的形式模型的集合。

一个属性是一组满足这一属性的语义模型。的满意度一个系统(更准确地说，是它的语义)的一个规范，它可以等价地定义为证明它的最强属性是系统的一个属性的证据，称为其收集语义。

一个例子是跟踪语义编程语言的。该语言中程序的语义将所有可能的程序执行描述为对给定可能状态集中所选状态的一组跟踪。跟踪中的两个连续状态对应一个基本的程序计算步骤。属性的一个例子是终止属性，该属性声明所有执行轨迹都应该是有限的。

形式化的验证方法很难付诸实践，因为复杂系统的语义和规范都很难定义。即使这是可能的，如果没有巨大的计算成本，证明也不能自动化(使用定理证明程序、模型检查器或静态分析器)。考虑所有可能的系统就更难了。因此，要么在小系统中工作(例如，模型检查)，要么考虑大系统的近似值(例如，抽象模型检查)。

抽象的解释。抽象的解释⁵是一种数学结构的合理近似理论，特别是那些涉及描述计算机系统行为的理论。为了证明一个性质，抽象思想是考虑集合语义的声音过近似值，待证明性质的声音过近似值，并在抽象上进行正确性证明。

对于自动证明，这些抽象必须是计算机可表示的，因此它们不是在具体的数学领域中选择的，而是在一个抽象的领域。对应关系由a给出具体化函数将抽象属性映射到相应的具体属性。形式验证是不可确定的，抽象可能是不可确定的不完整的也就是说，它生产假警报，当一个具体的属性成立，但这不能在给定的抽象的抽象中得到证明，因此必须对其进行细化。的抽象函数是具象函数的反函数。它将具体的属性映射到它们在抽象域中的近似。应用到计算机系统的收集语义中，它正式地提供了系统属性的抽象。抽象验证方法包括设计一个足够粗的抽象函数，使抽象收集语义可以被计算机表示并有效地计算，并且足够精确，使抽象收集语义包含规范。

迈克尔·杰克逊:首先，正式模型的开发是一项工程任务。在已建立的工程分支中，挑战是通过在每个特定产品类别中积累的经验来解决的，并在正常的设计规程中捕获。

抽象解释使关于抽象的直觉形式化。它允许系统地产生声音推理方法而且有效的算法在计算机科学的各个领域(语义、验证和证明、模型检查、静态分析、程序转换和优化、类型化或软件隐写术)中近似不可确定或高度复杂的问题。目前它的主要应用是在复杂硬件和软件计算机系统的安全和安全方面。

静态分析验证。静态代码分析通过直接检查描述系统的源代码或目标代码的语义(不执行程序，如动态分析)。通过有效地计算系统的集合语义的抽象来进行抽象证明。在工业环境中使用的成功静态分析器的例子有aiT (www.absint.com/ait用于计算最坏情况执行时间的过近似值⁸)和Astrée (www.astree.ens.fr用于计算收集语义的过近似值，以证明不存在运行时错误⁶)。

它们越来越成功的原因是它们有用(例如，它们解决了实际问题)、可靠(它们的结果可以被信任)、非侵入性(最终用户不必改变他们的编程方法(例如，通过生成可以直接从程序文本中派生的规范和抽象语义)、现实(适用于任何奇怪的工业环境)、可扩展(可在实际工业代码中发现的数百万行代码)、而且是结论性的(很少或没有虚惊一场)。

基于语言的语义和抽象的设计非常困难，但在定义良好的程序家族(例如，同步的、时间触发的、实时的、安全关键的、为Astrée用C编写或自动生成的嵌入式软件)上是可能的。Astrée的抽象是通过连接许多简单抽象来设计的，这些基本抽象单独来说很容易理解和实现。在出现假警报的情况下，每个抽象都可以通过参数和抽象指令(它们在代码中的包含可以自动化)调整成本和精度。如果现有的抽象不能解决虚警问题，那么可以很容易地加入新的抽象来扩展和改进抽象之间的连接。因此，抽象不变量可以在几个精化步骤中得到加强，直到没有虚警。⁷

回到顶部

Byron Cook:并发系统的验证

许多关键的应用程序涉及高度的并发性，因此许多活动彼此并行地进行。并发性可以在并发组件之间创建异常复杂的交互，使得验证问题本质上更加复杂。

传统的计算机系统的指定和自动推理方法已不能满足并行系统的要求。它们不考虑其他并发组件造成的副作用、多个同时发生的事件或进程之间为确保数据完整性所需的同步，等等。有效核查通常需要专门的工具。

例如，考虑线程终止。并发程序通常设计成在关键线程中执行的某些函数必须终止。这些功能可以在操作系统、Web服务器和电子邮件客户端中找到。到目前为止，还没有已知的自动程序终止证明程序支持证明线程终止的实用方法。

另一个例子是，并发程序通常是用假设但不保证内存安全的语言编写的(例如，指针解引用永远不会失败，内存永远不会泄漏)。同样，到目前为止，还没有已知的自动程序验证器支持对并发程序的内存安全性进行验证。

最近的进展现在允许我们解决这些问题(例如，证明诸如内存安全和并发代码的终止等属性)。这些改进导致最近在终结者终止证明程序中增加了对并发性的支持¹⁵以及SLAyer形状分析引擎。¹⁴

BYRON COOK:并发性可以在并发组件之间创建异常复杂的交互，使得验证问题本质上更加复杂。

这些进步的共同主题是线程模块化:如果可以找到适当的抽象来表示并发系统中的其他线程，则可以使用现有的顺序程序证明程序来证明并发程序的正确性。在终止证明的情况下，抽象描述了由系统中其他线程引起的值的变化方向(称为方差)。例如，我们可能知道变量的值x不能在其他线程中向上，因此允许我们证明在相关线程中递减的循环的终止x在每个循环迭代过程中。在内存安全证明的情况下，抽象描述了锁和数据结构之间的关联:我们可以通过假设某些数据结构只有在获得相关的锁时才可以安全地修改，来证明相关线程的内存安全。

线程模块技术的困难在于抽象空间太大，因此很难为给定的程序验证问题找到正确的抽象空间。必须开发启发式。此外，通过使用实验评估，必须证明这些启发式在常见情况下有效。我们已经开发并评估了这种启发式。在终止证明的情况下，我们发现通过暂时忽略并发性，我们可以猜测一组排序函数(参见Patterson)¹³获取详细信息)，这将导致一个有用的候选抽象。使用静态程序分析技术，我们可以证明，例如，其他线程中的每条指令都不会增加x。这一事实x不需要增加，相反y，来自于通过顺序程序终止证明程序的终止证明(参见Cook⁴的详细信息)。

在证明内存安全性的情况下，我们使用将锁与变量匹配的初始猜测，然后使用反例引导的技术来优化受锁保护的数据结构的形状(参见Gotman)⁹为进一步的细节)。

回到顶部

结论

软件密集型系统的可靠性只能通过应用可靠的设计原则来实现。反过来，这是通过对产品的理解和工程师在特定领域、产品类型和技术方面的专业化来实现的。抽象解释可以帮助减少证明复杂软件系统的属性和正确性所固有的复杂性，否则这是不可实现的。这种方法促进了自动化推理和完全自动化推理。特别是，最近验证技术的进步使验证并发系统和通过考虑线程的终止来证明终止成为可能，而不考虑并发性本身。

在形式方法的领域，我们也会遇到激进的和正常的工程，以及介于两者之间的整个中间阶段的光谱。从某种意义上说，激进设计与常规设计的比率可以作为一个工程领域成熟度的衡量标准。

回顾过去，形式方法的激进工程已经成为该领域前20年的特征，使其成为一门艺术:它被限制在少数用户的有限范围内，以及少数高预算、高风险的项目，对这些项目来说，高保证是非常重要的。今天的情况已经不同了:

• 从弱形式方法到强形式方法的第一次转变¹⁷将这个领域从仅仅规范转向基于工具的语义分析，使形式方法不仅具有描述性，而且具有可操作性。
• 第二个转变是将工具支持从重量级的形式方法转移到轻量级的形式方法:从仍然需要专业技能、教育和大量直觉的证明助手，到嵌入软件工程师通常开发环境中的全自动分析。

这种转变对于使每个软件开发人员能够无缝地使用技术至关重要，从激进的设计工作推进到日常实践。这样一来，它就不再是一门艺术，只是另一门手艺，就像摄影使每个人都能以非常合理的成本，不需要成为或求助于肖像画家，就能描绘出一个完全忠实于主题特征的主题一样。

我们观察到，今天不同的技术在这个过渡轴上占据了不同的位置。虽然并发系统的终止证明仍然是一门艺术(激进设计的一个例子)，但类型检查等技术在绝大多数编程环境中都得到了加强(自然设计)，而且许多其他技术正在走归化的道路。这是一条陡峭狭窄的道路，需要几十年的时间才能走完。例如，抽象解释是在20世纪70年代被发现的，但是直到最近几年，我们才有了诸如Astrée这样的工具，使普通开发人员能够在增强的正常工程过程中将复杂的抽象解释集合作为他们日常工作的一部分应用。模型检查，今年被奖励为ACM A.M.Edmund M. Clarke, Joseph Sifakis和E. Allen Emerson获得的图灵奖是形式化方法的又一个成功的例子，在他们25年以上的历史中，形式化方法变得越来越自然。一旦归化，一种技术(及其大师)的魔力就会消失，但我们都能从进入主流生产的革命者的成就中获益。

正如12年前所指出的，高保证系统的专业化涉及设计适当的异构方法，以充分利用问题的各种特定于应用程序的特性。¹⁶计算机辅助工程方法是新工艺。它的目标是理解和解决问题不同类地在元层面，整个方法和范式被结合在一起。尽管这一点已经适用于许多顺序系统，但对于分布式系统尤其如此，因为分布式系统本质上具有更高的概念复杂性。笔记本电脑中的多核体系结构和作为Web计算和云计算环境一部分的大规模多核系统需要更多的关注。

这个任务仍在继续……

回到顶部

回到顶部

回到顶部