Table of Contents

The Importance of Formal Specification

形式化规范的重要性

当处理非常复杂的系统时，寻找bug变得更加困难。虽然有各种各样的工具可以帮助你，但这些工具主要是帮助确定为什么会发生错误。作为一个行业，我们在帮助你从一开始就避免出现漏洞方面做得很少。

这是为什么呢？在某种程度上，我们仍然习惯于把bug看作是代码中的错误–未捕获的空值、偏离一等等，但是最微妙和最危险的bug是设计上的问题。它们是当所有的东西都是局部正确的，但以一种全局不正确的方式进行交互的情况。

考虑混合错误重试和滚动部署。客户端的初始请求和第一次重试可以由运行不同版本代码的不同服务器处理。任何意外的行为都不是客户端、服务器或负载均衡器的错，而是来自它们之间的相互作用。

没有人犯过错。每一个本地组件都在做我们告诉它要做的事情。鉴于系统的复杂性，在全局层面上理解这些行动的后果变得很困难。

处理这些问题的唯一方法是通过智能专家的努力工作。我们。但正如我们有工具帮助我们写代码一样，我们也有工具帮助我们写设计。一种强大的技术是写一个系统的软件模型，然后模拟这个模型的错误。

因为我们只对系统进行建模，而不是实现它，所以我们可以用编写代码的一小部分时间写出一个高层次的概述。然后我们可以使用工具来检查它是否满足我们的系统要求。这就是所谓的形式化规范【1】，也被称为可调试设计。形式化的规范可以帮助你成功地进行前期设计，节省时间、金钱和理智。

这可以通过两个例子看出来。通过使用形式化规范，亚马逊能够在DynamoDB中发现一个35步的错误，这个错误在广泛的设计审查、代码审查和测试中被忽略了。Rackspace公司在一个项目的后期应用了形式化规范，发现了一个需求不匹配，要求他们重新做一年的工作。一个编写嵌入式操作系统的团队发现，编写形式化规范使他们的整体代码大小减少了10倍。

如果形式化规范是如此强大，为什么人们不使用它呢？主要是由于社会原因。形式化规范的大部分工作都集中在一些高优先级的技术上，如电信和芯片组。在过去的半个月里，随着软件变得越来越关键，越来越复杂，我们已经意识到它有更广泛的潜力，可以使关键系统之外的软件工程师受益。

形式化规范并不能创造奇迹。它不会为你写代码。它不能取代我们作为工程师的技能，但它是一种强大的手段，可以在我们花几个月时间建造系统之前，在我们凌晨3点被叫醒处理故障之前，发现系统中的错误。你不会在没有蓝图的情况下建造一座房子。为什么你会在没有蓝图的情况下建造一个价值百万美元的系统呢？

我们如何构建本书的结构

SRE虽然涉及复杂的技术系统，但归根结底是一种文化实践。文化是人的产物，这启发我们根据你在组织中的SRE数量来组织本书的各个部分–你具体处理什么，你的一天是怎样的，取决于有多少个SRE工程师。我们将本书的文章分为 “SRE新手” 、0-1个SRE、1-10个SRE、10-100个SRE和 “SRE的未来 ”。

读者如果想找寻先从哪里开始的指导，可以直接跳到最适用于自己的部分；但是，你仍然会发现阅读那些目前并不适用于你日常的部分的文章的价值。

在0到1个SRE时，还没有人被指定为SRE，或者你已经找到了你的第一个SRE，这个角色看起来几乎是孤独的。

在1到10名SRE时，你正在组建一个团队，有知识共享和分工的能力。

在10到100个SRE时，你已经成为一个组织，你需要思考的不仅仅是你所从事的系统，还需要思考如何组织这么多SRE。

“SRE新手” 涵盖了基础性的话题（尽管并不详尽！），对于那些刚刚开始SRE之旅的人来说是很有帮助的，即使是最有经验的SRE，也是一种复习。 “SRE的未来” 包含了一些文章，这些文章探讨了SRE潜在的发展方向，或者是（目前）坐拥时代潮流。

没有必要按照任何特定的顺序阅读本书。你可以从头到尾读一遍。或者，如果你对某个特定的主题感到好奇，可以翻到索引，在那里你可以找到关于该主题的所有文章。把它作为参考指南，或者是灵感的来源–可以在需要的时候提供一个震撼。或者，也许可以建立一个阅读俱乐部，每周一次挑选一篇文章与同事讨论。这就是散文集的魅力所在。我们希望你和我们一样喜欢阅读它们。

结语

SRE系列的文章，有时间我就会翻译一些，希望大家能学到对自己有用的东西。谢谢

翻译不易，转载时请注明原文链接，谢谢

延伸阅读

1.formal specification
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools.[1][2] These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.[3]