反应系统的建模规约与验证

Ｌ．埃斯托等

计算机科学建造人工制品，这些人工制品应为用户提供某些明确的服务。它们正确地完成所担负目的的行为规约是至关重要的。确定计算系统是否确实提供了由它的规约所描述的行为问题叫做正确性问题，它是计算机科学中最基本的问题。研究描述计算机模型及它们的规约，以及根据它们的规约建立系统正确性的方法(有可能是自动的)，叫做算法验证。

一个反应系统是由计算组件网络组成的，并且通过在它们自身及所处环境的交互使用来达到它们的目的。因此甚至相对小的系统也有可能展现意想不到的复杂行为，而且由于反应系统经常被用于安全关键系统，因此对基于数学的形式方法学需求是不断地增强。

本书向研究生提供了更为全面的介绍，描述了各种各样的方法，各种方法的优缺点以及何时使用它们最佳。

本书介绍了米尔纳的通讯系统演算(ccs)和它的操作语义学，连同建立在互模拟技术基础上的等价概念和亨尼斯一米尔纳逻辑(HML)的递归扩展。本书的第二部分中所介绍的理论被拓展到考虑时间问题。

本书共有13章，分成二大部分。第一部分反应系统的经典理论，含第1～7章。1.绪论；2.CCS语言；3.行为等价；4.固定点理论与互模拟等价；5.HML；6.HML与递归；7.建模互斥法算法。第二部分实时系统理论，含第8～13章。8.入门；9.CCS与时间延迟；10.计时自动机；11.计时行为等价；12.HML与时间；13.建模与费希尔算法分析。最后是附录A对学生项目的建议。本书的内容是建立在作者过去6年左右在丹麦Aalborg大学和冰岛的雷克雅未克大学所开设的课程之上的，它向学生提供了一个对该领域的广泛介绍。

本书引导读者理解并掌握过程代数，是一本出色的大学高年级教课书。