Event-B建模 系统和软件工程

作者简介

简-埃蒙德·阿布瑞尔（Jean-Raymond Abrial） 法国计算机科学家，国际知名的形式化方法和软件工程专家，欧洲科学院院士。20世纪80年代，他先后开发了著名的Z语言和B方法。2000年以后，他开发了Event-B方法，并领导一个国际团队，在欧盟项目支持下，为Event-B开发了公开免费的Rodin平台。这些语言和方法被国际形式化方法领域广泛接受和使用，并被开发工作者应用于软件和其他系统的实际开发工作。阿布瑞尔教授长期致力于推动和参与形式化方法的工业应用，指导了B方法在轨道交通领域的最早开发工作，在相关领域做出了卓越的贡献。阿布瑞尔教授与国内一些高校和研究单位有长期而密切的合作关系，并于2016年获得了中华人民共和国国务院颁发的“中华人民 共和国国际科学技术合作奖”。

内容简介

Event-B是一种基于传统的谓词演算和定理证明的形式化语言,支持逐步精化地建立系统模型,适合于实时性强的嵌入式控制系统的建模，多用于工业软件系统的开发，本书为Event-B的开发者Jean-Raymond Abrial关于形式化方法的著作。 1.作者是国际著名软件和软件理论专家，首次将“B方法”系统级的工控软件高安全保障解决方案引入中国，这是目前市场上唯一的一本关于Event-B的中文书籍。 2.书中包含了大量具有不同难度的练习和开发项目，方便读者对所学知识进行检验和实践。 3.书中每个例子都用Rodin平台工具集证明过，因此书本的内容十分严谨。 4.外文原版书是这一领域极具权威的教材书籍，由剑桥大学出版社出版，内容方面有很高的质量保障。