工业关键系统的形式化方法：应用综述.pdf

国际信息工程先进技术译丛 工业关键系统的形式化 方法：应用综述 ［意］ StefaniaGnesi TizianaMargaria 　著 　　靳添絮　连晓峰　等译 机械工业出版社 　　形式化方法以数学为基础，其目标是建立精确的、无二义性的语义， 对系统开发的各个阶段进行有效的描述，使系统的结构具有先天的合理性、 正确性和良好的维护性，能较好地满足用户需求。本书记录和展示了作者 关于形式化方法如何在工业关键系统中进行应用的研究成果。 本书分为6部分：第1部分是概述；第2部分致力于介绍建模范例； 第3部分介绍了包括形式化方法和相关工具的使用以及应用程序在实际系 统领域的发展；第4部分则向读者展示了形式化方法在通信系统中的发展 和成果；第5部分则介绍了形式化方法在互联网和在线服务方面的应用； 而在第6部分则介绍了实时应用程序的形式化方法。 本书可用作高等院校计算机科学、自动化相关专业本科生、研究生以 及教师的参考用书，也可作为业内专业人士的参考书。 译　者　序 形式化方法以数学为基础，对系统开发的各个阶段进行有效的描述，是有效 验证系统设计和开发正确性的重要手段之一。让已经被普遍应用于测试方法复杂 且对安全性有很高要求的控制系统的形式化方法更好地融入工业中，并使得它们 在那里可以发挥最大的作用，这也是译者翻译本书的初衷。 本书作者是StefaniaGnesi和TizianaMargaria。其中，StefaniaGnesi之前在佛 罗伦萨大学任教，主讲针对软件系统分析和规范的方法和工具，现在是意大利比 萨ISTI-CNR的一位形式化方法和工具实验室的领导。而TizianaMargaria则是波 茨坦大学数学和自然科学学院的一位教授，在那里她负责信息学院的服务和软件 工程学科，也曾在德国哥廷根（Göttingen）大学、多特蒙德工业大学、帕绍大 学，以及瑞典和意大利的大学游历过。应该说，作者在形式化方法在工业关键系 统应用方面是有很深研究的。 本书分为6部分：第1部分是概述；第2部分致力于介绍建模范例；第3部 分介绍了包括形式化方法和相关工具的使用以及应用程序在实际系统领域的发 展；第4部分则向读者展示了形式化方法在通信系统的发展和成果；第5部分则 介绍了形式化方法在互联网和在线服务方面的应用；而在第6部分则介绍了实时 应用程序的形式化方法。 本书第1～3章由靳添絮翻译，第4～7章由连晓峰翻译，第8章由董美华、 胡冰川、班岚和金成学翻译，第9章由胡波、周锐、王佩荣和潘媛翻译，第10 章由苑昆、郑舒阳、贾琦和毋冬翻译，第11章由陆亚灵