软件可靠性方法前言

前言

许多书籍描述了如何使用形式化方法来提高软件质量. 但是，大多数书籍都围绕一种特定的方法，并将其用作解决软件可靠性问题的推荐解决方案. 本书通过大量的形式符号表示和技术为读者提供了对形式方法的更全面描述. 该书将比较它们之间的差异，并讨论它们的优缺点.

形式方法的主要挑战之一是如何将研究人员开发的技术传播到软件开发社区. 最近，我们似乎对形式化方法工具的重要组成部分有了更好的了解. 事实证明，这种工具越来越被软件和硬件开发行业所接受. 理想情况下，形式化方法必须直观地使用（***是使用图形界面），不需要用户花费大量的学习时间，并且在开发过程中只需花费相对较小的额外费用. 与10或20年前相比软件可靠性方法，形式化方法更容易为人们所接受，这在硬件领域尤其重要. 但是，不同方法之间仍然存在激烈的争论.

这本书通过一系列技术着重介绍形式方法的主要原理. 在撰写本文时，本书中并未包含许多高级技术. 这些先进技术涉及实时系统和混合系统，描述协议的形式化系统，以及一些特殊的数据结构，例如二进制决策图. 本书没有包括这些特定技术，但这并不意味着本书中的方法要优于它们，而是因为本书中描述的算法和方法已应用于当前的软件可靠性工具. 这些方法的选择只是以的方式表达形式方法的主题. 但是，在选择时，总是不可避免地要选择一个更接近我研究方向的主题. 贯穿本书的主要内容是逻辑和自动机理论. 有兴趣的读者可以在相关章节之后列出的其他书籍和研究论文中找到这些高级方法的详细信息.

如果没有直接使用相关工具的实际经验，则形式方法的学习不完整. 本书包含大量的练习和项目，可以使用软件可靠性工具来完成. 本书还提供了多个章节中使用的一些连续性示例. 学习形式方法并了解其优缺点的有效方法是跟踪和理解这些横截面示例. 在某些情况下，后面的章节将详细介绍上一章的练习部分中提到的连续性示例. 这样做的另一个目的是帮助读者检查上一章中练习的答案（而不仅仅是提供明确的答案）. 鼓励读者检查他们对这些示例的直觉是否可以帮助改善他们对先前练习的答案.

本书提供的大多数练习和项目都可以通过某种工具进行选择. 尽管某些软件可靠性工具需要昂贵的许可费用，但许多工具仍允许出于非盈利目的免费使用. 要使用这些工具，通常需要从其网页下载并根据网页上的说明进行安装. 在相关章节之后列出了一些工具和相应的网页. 应该注意的是，即使某些工具可以在没有获得许可的情况下使用，它们也经常要求用户向工具开发者发送一封信，同意遵守该工具的使用条款. 在许多情况下，这些术语仅将工具限于学术用途，开发人员对使用工具可能造成的损坏不承担任何责任. 由于网页和URL经常更改，并且由于不断开发新的工具来替换现有的工具，因此，我不能保证本书所列网页上的信息始终有效. 此外，本书不能保证这些工具在任何环境下都能正常工作.

不同的群体对形式方法有不同的兴趣. 当然，写一本对项目经理，软件开发人员，质量保证团队和研究人员具有同样吸引力的书是不可能的，但是我仍然尝试在这本书中写. 添加读者群中每个人都感兴趣的内容. 因此，读者可以在阅读时跳过过于理论或技术性的章节. 应该注意的是，本书的重点主要是技术，而不是方法论.

在描述一些形式化方法的同时，本书还给出了相应的算法. 了解这些算法对于使用这些方法不是必不可少的，但是了解它们可以使您对这些方法的工作方式有更深入的了解. 本书省略了与本书形式方法有关的大多数数学证明，但有时也包含简短的证明，以增加读者的直观理解.

作者要感谢以下与本书相关的鼓舞人心的讨论和有用的建议的人: 尼娜·阿姆拉，克里斯特尔·拜尔，戴维·贝辛，Shai Ben-David，罗德里克·布洛姆，格伦·布朗斯，埃德·，丹尼斯水坝，杜小群，库萨·埃特萨米，艾米·费尔蒂，艾尔莎·冈特，道格·豪，奥娜·库普弗曼，巴特·克纳克，鲍勃·库山，本特·琼森，列昂尼德·利比金，安卡·穆斯乔尔，基达尔·南乔希，沃西切·彭奇克，卡维塔·拉维，纳塔拉扬尚卡·斯伦比，理查德Wolfgang Thomas，Moshe Vardi，Igor Walukiewicz，Thomas Wilke，Mihalis Yannakakis和Lenore Zuck. 实际上，写这本书最有意义的方面之一就是有机会从实践者和专家就特定主题给出的建议和评论中进一步学习.

我不是第一个引用刘易斯·卡罗尔冒险小说中的单词吗？但是，鲜为人知的是查尔斯·路德维希·道奇森（Charles Lutwidge Dodgson，笔名刘易斯·卡罗尔（Lewis Carroll）），是一位研究逻辑的视觉表示的数学家. 他的“胆大”（两个字母）和“三公”（三个字母）图是卡诺地图的前身. 卡诺地图可以通过一种易于教授和学习的方式来表达逻辑，这也是许多形式化方法研究的趋势.

Doron Peled

新泽西州莫雷山软件可靠性方法，2001年3月

本文来自电脑杂谈，转载请注明本文网址：
https://www.pc-fly.com/a/jisuanjixue/article-198755-1.html