反应系统的验证形式方法与算法

本书是施普林格出版社出版的《理论计算机科学教课书》丛书中的一本。该丛书是以理论计算机科学欧洲协会（EATCS）的名义出版的。计算机中重要的反应系统包括微处理器、计算机操作系统、空中交通管制系统、舰载控制系统和其他嵌人式系统，在实践中反应系统一般通过故障模式来表征。反应系统在它们布置之前必须先校正，因此现代信息处理系统，例如数字线路或协议的设计正在变得越来越困难，需要花费相当大的设计成本与时间（大约70％），以保证设计的准确。因此，设计系统已日益成为验证系统的同义语。对反应系统验证的研究，特别是对模型检查的研究是理论计算机科学非常成功的方法之一。但是涉及该方法的书籍（即使是很基础的）却很难找到。本书填补了这一空白，向初学者和研究人员介绍了大多数相关算法。

Verification of Reactive Systems