Real-Time Systems: Specification, Verification and Analysis

The field of real-time systems has not traditionally been hospitable to newcomers: on the one hand there are experts who seem to rely on experience and a few specialized documents and, on the other, there is a vast and growing catalogue of technical papers. There are very few textbooks and the most successful publications are probably collections of past papers carefully selected to cover different views of the field. As interest has grown, so has the community, and the more recent papers are spread over a large range of publications. This makes it particularly difficult to keep in touch with all the new developments.

If this is distressing to the newcomer, it is of no less concern to anyone who has to teach a course on real-time systems: one has only to move a little beyond purely technical concerns to notice how quickly the teachable material seems to disappear in a cloud of opinions and a range of possibilities. It is not that the field lacks intellectual challenges or that there is not enough for a student to learn. On the contrary, the problem seems to be a question of where to start, how to relate practical techniques with methods of analysis, analytical results with theories and, more crucially, how to decide on the objectives of a course.

This book provides a detailed account of three major aspects of real-time systems: program structures for real-time, timing analysis using scheduling theory and specification and verification in different frameworks. Each chapter focuses on a particular technique: taken together, they give a fairly comprehensive account of the formal study of real-time systems and demonstrate the effectiveness and applicability of mathematically based methods for real-time system design. The book should be of interest to computer scientists, engineers and practical system designers as it demonstrates also how these new methods can be used to solve real problems.