| Prof. Kim Guldstrand Larsen, Aalborg University, Denmark | Embedded systems are finding their way into nearly every aspect of our daily lives, and often in highly safety-critical applications, where hard timing constraints are to be met. At last we have the book on the design of real-time systems which successfully combine mathematical models of systems with that of their practical implementation and automatic verification using state-of-the-art model checking. The exposition provides and exceptionally clear and self-contained account of some of the most mature formalisms, methods and tools for modeling, analyzing and constructing real-time systems. The book can be used readily at several levels of computer science and engineering educations, and will be of equal inspiration for the theory and engineering inclined student. |
| Prof. Tony Hoare, Microsoft Research Ltd Cambridge, UK |
In 1989 I had the privilege of working with the first author on the
EU-funded basic research project ProCoS (Provably Correct Systems).
Our task was to develop proof technology for the design, development
and implementation of error-free software, particularly programs
for real time and interactive control systems. Our goal was to
ensure there were no gaps in the technology, because gaps are
where errors will congregate and multiply.
Since the completion of the Procos project in 1995, the authors and their colleagues have made further spectacular progress. They have unified the various relevant theories to eliminate the risk of gaps; and they have implemented the theories as a chain of programming support tools, to extend the benefit of theory to practicing programmers. This book reports the success of both the original ProCoS project and of the further work. I can recommend it to all researchers in the field of verified software. It demonstrates an effective collaboration of theorists and tool-builders from many countries working together over a long period. It shows how theories can be elegantly unified, and how tools can be soundly based on theory, and seamlessly integrated. I hope the book will inspire many researchers to raise their level of ambition to cover the wider fields of application of verification technology. |
| Prof. Amir Pnueli, Weizmann Institute of Science; Israel and New York University |
The book on real-time systems by Olderog and Dierks presents a unique
contribution to the state-of-the art in the application of formal
methods for the development of real-time and embedded systems. It is
the first text that presents a complete and well-rounded process for
the systematic development of real-time systems supported by formal
methods and automated tools, whenever possible. The proposed
development flow proceeds through several levels of description, and
provides sound methods and tools for establishing the consistency and
compatibility between the description on each two consecutive levels
or, alternatively, methods for the automatic translation
(compilation) from one level to the next. This introduces a method for
seamless development of correct and reliable real-time systems.
The various levels recommended in the text proceed from the requirement level which uses the very expressive general form of the duration calculus. It then proceeds to narrow the specification language to more restricted forms which admits better decidability properties. At the design level, the authors propose the use of Programmable Logic Controllers (PLC) automata. which can then be either used directly for certain types of hardware implementations, or translated into C programs with timers. The main tool for automatic verification is the versatile formalism of timed automata, and the book provides translation of all involved stages in the development into this common format, as well as an excellent guide for the use of the UPPAL tool for carrying out the necessary verification tasks. Altogether, the book is very well written and remarkably motivated. It contains a large amount of impressive theoretical results, in particular in the parts related to the Duration Calculus. On the other hand, it can be used in a modular way as the basis of courses that either emphasize the more practical and pragmatic aspects, or concentrate on a more theoretic study of the involved concepts of real-time semantics and modeling. It is an excellent text that covers a very important topic in which appropriate texts are almost non-existent in a most professional and rigorous, yet practically appealing, style. |
| Prof. Anders P. Ravn, Aalborg University, Denmark | Here is a very useful book for graduate and research students in the embedded systems area. It introduces three complementary views on a system: Duration logic formulae for requirements, timed automata for design models, and PLC-automata for implementations, and it does more than dumping them on the reader; it links them semantically and through translation processes such that they indeed are views of the same system. The text comes with instructive exercises and introductions to state of the art design and analysis tools for the two automata formalisms. An added benefit is that students will learn from the text how to give a semantics to a notation in a complete and consistent way without undue fuss or strained notational conventions; that is a facet which may be appreciated by many research students struggling with concrete notations of similar kinds. |
| Prof. ZHOU Chaochen, Chinese Academy of Sciences, Beijing, China | This book represents a great step towards industrial application of formal methods in the area of safety critical real-time systems. It thoughtfully chooses Duration Calculus (DC), an Interval Temporal Logic based real-time calculus, as requirement specification language, and Programmable Logic Controllers (PLCs), a hardware widely used in automation industry, as implementation platform. To bridge these two distant subjects, it adopts DC Implementables, Constraint Diagrams and PLC-Automata at different abstract levels of system design. The strength of the bridge is guaranteed by a unified DC semantics of each block above. The accessibility of the bridge is supported by various pictorial notations and tools, including UPPAAL and MOBY/RT. The former can verify system properties when translating the blocks into Timed Automata and the latter transforms PLC-Automata into programs executable on PLCs. This book gives you not only knowledge of the theories involved, but also remarkable insights how to make theories practically useful. Researchers who want to contribute to further development of software engineering into a true engineering science are strongly advised to read this book. |
