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
