[实时系统,形式化描述和自动验证] 形式化验证

　　Ernst-Rudiger Olderog University of 　　Oldenburg, Germany 　　Henning Dierks University of Oldenburg,
　　Germany
　　Real-Time Systems
　　Formal Specification and Automatic
　　Verification
　　2008, 320pp.
　　Hardcover
　　ISBN 9780521883337
　　
　　E.R. Olderog著
　　实时系统是一种带有时间约束的计算机系统,这些系统许多动作的完成是与时间相关的,即要满足一定的时间限制,它需要在特定的时间范围内的对某些输入及时做出反应。例如,碰撞中汽车的安全气囊须在300毫秒膨胀开。它的许多嵌入式应用,都有一个共同的特点就是对实时性、安全性要求很高,都需要实时的形式化规范技术。
　　在本书中,作者介绍了三种技术,均基于逻辑学与自动机,包括时段演算、时间自动机和PLC自动机。这些技术的汇集,从时段演算的实时要求描述,到被PLC自动机规范的设计,再到嵌入式系统硬件平台的源代码,形成了一个无缝的设计流程。书中还介绍了形式化描述技术的语法、语义和验证方法,属性的建立以及生活中的应用实例等。全书分6章,1. 简介,介绍什么是实时系统以及它的属性,最后还给出了一些应用实例和练习;2. 时段演算,包括它的语法、语义和验证方法、验证规则等;3. 时段演算的属性和子集;4. 时间自动机,介绍了时间自动机模型、时间自动机网络的语法和语义,还给出了一种以时间自动机作为行为模型的模型验证工具UPPAAL,并对一个经典的实时系统实例进行了验证;5. PLC的自动机,讲述什么是PLC及PLC自动机,并分析了PLC源码的转化等问题;6.自动验证,介绍了自动验证方法、实时性要求、设计规范以及实际验证和常用工具。
　　本书每个章节的结尾都提供了详细的个案研究和练习,分析了目前许多先进的实时系统的各个方面。因此本书不仅理论性强,同时也非常注重联系实际,非常适合实时系统或嵌入式系统相关领域的研究人员和学生使用,也可作为运输和自动化专业研究人员的阅读参考资料。
　　作者E.-R. Olderog是德国奥尔登堡大学计算机科学系的教授,1994年被授予德国研究理事会的莱布尼兹奖。H. Dierks研究员,目前也正与OFFIS(德国奥尔登堡计算机科学技术转让研究所)开展合作性研究。
　　赵俊娟,
　　博士生
　　(中国科学院电子学研究所)
　　Zhao junjuan,Doctoral Candidate
　　(Institute of Electronics,CAS)