《软件工程形式化方法综述：语言、方法与应用领域》

《Formal Aspects of Computing》：Review on Formal Methods for Software Engineering: Languages, Methods, Application Domains

形式方法在软件工程中的系统性应用与实践指导。本书以CSP、CASL等方法论为核心，通过247个实例和工具网站链接，探讨并发系统建模、电子合同验证、人机交互分析及安全协议设计等应用场景，强调数学严谨性与教育实践结合，旨在推动形式方法在工业界和教学中的普及。

　　

这本书由Markus Roggenbach、Antonio Cerone、Bernd-Holger Schlingloff、Gerardo Schneider和Siraj Ahmed Shaikh共同撰写，为研究生和本科生课程提供了软件工程方面的教学材料。它适用于那些希望教授软件设计和形式化验证中正式方法及工具有效应用的教师，同时也适合刚开始攻读博士学位的学生。唯一的先修要求是具备一些基础的数学符号知识，这类知识通常在计算机科学本科课程的早期阶段就会教授。

本书的核心内容分为三个部分，每个部分包含若干独立章节，并且每个部分都有一章作为开头和结尾。开篇的第1章对什么是形式化方法进行了总体介绍，并探讨了它们在软件工程和工业实践中的作用。第一部分“语言”部分具有基础性，为后续章节提供了参考；第2章定义了计算机科学中常用的几种用于系统规范和分析的逻辑语言；第3章介绍了专门用于并发系统建模和分析的过程代数CSP。第二部分“方法”部分在第4章展示了通用代数规范语言CASL，并在第5章讨论了一种基于规范的形式化（黑盒）测试方法。第三部分“应用领域”部分则讨论了三种基于形式化方法解决实际工程软件问题的具体案例；第6章描述了一种基于形式化逻辑的（电子、法律）合同规范及（运行时）分析方法；第7章回顾了基于形式化逻辑和CSP的系统规范及（认知、故障）分析方法（特别是涉及用户交互的情况）；第8章展示了如何使用CSP来设计和验证安全协议，尤其是认证属性。最后，第9章从历史角度总结了软件工程中的形式化方法，概述了这些方法及工具的发展历程以及对该领域产生重要影响的代表人物。

本书的写作风格非常易于理解，其中示例（247个）远远多于定义（63个）。¹作者们显然为这一成果感到自豪，因为书中例子的数量远多于图表的数量（这其实并不常见）。这些示例分布在各个章节中，涵盖了形式化方法在软件工程中的实际应用，尤其涉及当前计算机系统与软件领域的三大趋势：普适性、关键性和以用户为中心的设计理念。此外，书中还强调了工具的使用，并通过配套网站提供了相关练习和工具链接。²每一章除了常规的科学参考文献外，还附有注释书目以及关于当前研究方向的介绍，有时会提及该领域的核心会议系列和期刊。虽然书中选择的形式化方法和工具可能存在争议，但作者们的选择是合理且连贯的：第1章和第2章预先介绍了CSP，第3章对其进行了详细讲解，第7章和第8章中则将其应用于实际场景；第1章预先提到了CASL，第2章对其进行了初步介绍，第4章进一步详细阐述，第5章中进行了应用；第1章预先提到了PAT，第2章对其进行了介绍，第7章中进行了应用。

实际上，这本书还有三位其他作者：Liam O’Reilly合写了第4章，Hoang Nga Nguyen合写了第8章，而John V. Tucker则撰写了最后的第9章。

作者们提出了很高的期望，他们希望“他们在软件工程中提倡的形式化方法能够发挥积极作用并成为新的行业标准。”这句话中的大写体现了作者的专业背景——他们本身就是形式化方法领域的专家，而非单纯的软件工程师。这一关注点从Manfred Broy撰写的前言中得到了印证，他获得了2018年Formal Methods Europe颁发的FME Fellowship奖。³正如Manfred Broy所认为的（我也与作者们持有相同观点：2）：“每位计算机科学家都应该了解形式化方法。”⁴“更重要的是，不了解形式化方法诸多优势的软件开发人员根本不能被称为真正的计算机科学家或软件工程师。”¹作者们还希望这本书能引起实际工程师的兴趣，帮助他们理解如何将形式化基础和严谨方法应用于日常开发工作中。

作者们在书中呼吁在工业界广泛使用形式化方法来开发高质量软件（不仅限于安全关键型应用），并强调形式化方法教育是实现这一目标的关键。这与近期相关文献的观点一致。¹, 3, 5最后，作者们希望这本书能通过改进教育来推动形式化方法在软件工程实践中的应用。我相信这确实有可能实现。教授形式化方法往往具有挑战性，尤其是在选择合适的工具和示例方面。而这本书通过具体且引人入胜的例子，提供了一种严谨的数学方法论。