Tiempo Real

Real-time Systems Specification, Verification and Analysis
Edited by Mathai Joseph
Tata Research Development & Design Centre

Revised version with corrections June 2001

Original edition published in 1996 by Prentice Hall International, London, under ISBN 0-13-455297-0 This version incorporates corrections to and changes from the original edition.

This version is made available forresearch, teaching and personal use only. Copies may be made for noncommercial use only. Enquiries for other uses to the Editor (mathai@pune.tcs.co.in).

Contents

Preface Contributors 1 Time and Real-time Mathai Joseph Introduction 1.1 Real-time computing 1.2 Requirements, specification and implementation 1.3 The mine pump 1.4 How to read the book 1.5 Historical background 1.6 Exercises 2 FixedPriority Scheduling – A Simple Model Mathai Joseph Introduction 2.1 Computational model 2.2 Static scheduling 2.3 Scheduling with priorities 2.4 Simple methods of analysis 2.5 Exact analysis 2.6 Extending the analysis 2.7 Historical background 2.8 Exercises iii

vii xii 1 1 2 3 5 11 12 14 15 15 16 18 19 20 24 29 30 31

iv 3 Advanced Fixed Priority Scheduling Alan Burns and Andy WellingsIntroduction 3.1 Computational model 3.2 Advanced scheduling analysis 3.3 Introduction to Ada 95 3.4 The mine pump 3.5 Historical background 3.6 Further work 3.7 Exercises 4 Dynamic Priority Scheduling Krithi Ramamritham Introduction 4.1 Programming dynamic real-time systems 4.2 Issues in dynamic scheduling 4.3 Dynamic priority assignment 4.4 Dynamic best-effort approaches 4.5 Dynamic planning-basedapproaches 4.6 Practical considerations in dynamic scheduling 4.7 Historical background 4.8 Further work 4.9 Exercises 5 Assertional Specification and Verification Jozef Hooman Introduction 5.1 Basic framework 5.2 The mine pump 5.3 Communication between parallel components 5.4 Parallel decomposition of the sump control 5.5 Programming language 5.6 The mine pump example: final implementation 5.7 Furtherwork 5.8 Historical background 5.9 Exercises

CONTENTS
32 32 32 38 50 53 64 64 65 66 66 69 75 76 80 83 90 93 94 95 97 97 98 105 109 114 122 131 136 138 141

CONTENTS
6 Specification and Verification in Timed CSP Steve Schneider Introduction 6.1 The language of real-time CSP 6.2 Observations and processes 6.3 Specification 6.4 Verification 6.5 Case study: the mine pump 6.6 Historical background6.7 Exercises 7 Specification and Verification in DC Zhiming Liu Introduction 7.1 Modelling real-time systems 7.2 Requirements 7.3 Assumptions 7.4 Design 7.5 The basic duration calculus (DC) 7.6 The mine pump 7.7 Specification of scheduling policies 7.8 Probabilistic duration calculus (PDC) 7.9 Historical background 7.10 Further work 7.11 Exercises 8 Real-time Systems and Fault-tolerance HenkSchepers Introduction 8.1 Assertions and correctness formulae 8.2 Formalizing a failure hypothesis 8.3 A proof rule for failure prone processes 8.4 Reliability of the mine pump 8.5 Soundness and completeness of the new proof rule 8.6 Historical background 8.7 Exercises References Index

v 147 147 147 156 162 164 169 178 180 182 182 182 184 188 189 191 198 202 205 224 225 227 229 229 230 232 234 236 250254 256 259 272

Preface

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 paperscarefully 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...