Prentice Hall Software Engineering 2001 Real time Systems Specification Verification and Analysis Joseph Mathai.pdf

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 for research,
teaching and personal use
only.
Copies may be made for non-
commercial use only.
Enquiries for other uses to
the Editor
(******@).
Contents
Preface vii
Contributors xii
1TimeandReal-time 1
MathaiJoseph
Introduction 1
Real-puting 2
Requirements,specificationandimplementation 3
Theminepump 5
Howtoreadthebook 11
Historicalbackground 12
Exercises 14
2FixedPriorityScheduling–ASimpleModel 15
MathaiJoseph
Introduction 15
16
Staticscheduling 18
Schedulingwithpriorities 19
Simplemethodsofanalysis 20
Exactanalysis 24
Extendingtheanalysis 29
Historicalbackground 30
Exercises 31
iii
iv CONTENTS
3 AdvancedFixedPriorityScheduling 32
AlanBurnsandAndyWellings
Introduction 32
32
Advancedschedulinganalysis 38
IntroductiontoAda95 50
Theminepump 53
Historicalbackground 64
Furtherwork 64
Exercises 65
4DynamicPriorityScheduling 66
KrithiRamamritham
Introduction 66
Programmingdynamicreal-timesystems 69
Issuesindynamicscheduling 75
Dynamicpriorityassignment 76
Dynamicbest-effortapproaches 80
Dynamicplanning-basedapproaches 83
Practicalconsiderationsindynamicscheduling 90
Historicalbackground 93
Furtherwork 94
Exercises 95
5AssertionalSpecificationandVerification 97
JozefHooman
Introduction 97
Basicframework 98
Theminepump 105
109
positionofthesumpcontrol 114
Programminglanguage 122
Th