Real-time systems. Scheduling, analysis and verification

Scheduling, Analysis, and Verification......Page 1
CONTENTS......Page 9
PREFACE......Page 15
LIST OF FIGURES......Page 21
INTRODUCTION......Page 27
1.1 WHAT IS TIME?......Page 29
1.2 SIMULATION......Page 30
1.3 TESTING......Page 31
1.4 VERIFICATION......Page 32
1.5 RUN- TIME MONITORING......Page 33
1.6 USEFUL RESOURCES......Page 34
2.1.1 Propositional Logic......Page 36
2.1.2 Predicate Logic......Page 44
2.2.1 Languages and Their Representations......Page 54
2.2.2 Finite Automata......Page 55
2.2.3 Specification and Verification of Untimed Systems......Page 59
2.3 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 63
2.4 SUMMARY......Page 64
EXERCISES......Page 65
REAL- TIME SCHEDULING AND SCHEDULABILITY ANALYSIS......Page 67
3.1 DETERMINING COMPUTATION TIME......Page 69
3.2.1 Scheduling Preemptable and Independent Tasks......Page 70
3.2.2 Scheduling Nonpreemptable Tasks......Page 84
3.2.3 Nonpreemptable Tasks with Precedence Constraints......Page 85
Rendezvous Model......Page 87
3.2.5 Periodic Tasks with Critical Sections: Kernelized Monitor Model......Page 89
3.3.2 Scheduling Single- Instance Tasks......Page 92
3.3.3 Scheduling Periodic Tasks......Page 96
3.4.1 PERTS/ RAPID RMA......Page 98
3.4.2 PerfoRMAx......Page 99
3.4.3 TimeWiz......Page 100
3.5 AVAILABLE REAL- TIME OPERATING SYSTEMS......Page 101
3.6 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 102
3.7 SUMMARY......Page 103
EXERCISES......Page 110
MODEL CHECKING OF FINITE- STATE SYSTEMS......Page 112
4.1 SYSTEM SPECIFICATION......Page 113
4.2 CLARKE– EMERSON– SISTLA MODEL CHECKER......Page 115
4.4 APPLICATIONS......Page 119
4.4.1 Analysis Example......Page 120
4.5 COMPLETE CTL MODEL CHECKER IN C......Page 122
4.6.1 Binary Decision Diagrams......Page 142
4.7 REAL- TIME CTL......Page 146
4.7.1 Minimum and Maximum Delays......Page 147
4.7.2 Minimum and Maximum Number of Condition Occurrences......Page 149
4.7.3 Non- Unit Transition Time......Page 151
4.8 AVAILABLE TOOLS......Page 152
4.9 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 153
4.10 SUMMARY......Page 155
EXERCISES......Page 157
VISUAL FORMALISM, STATECHARTS, AND STATEMATE......Page 160
5.1.1 Basic Statecharts Features......Page 161
5.3 MODULE- CHARTS......Page 166
5.4.3 Code Executions and Analysis......Page 168
5.5 AVAILABLE TOOLS......Page 169
5.6 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 171
5.7 SUMMARY......Page 172
EXERCISES......Page 173
REAL- TIME LOGIC, GRAPH- THEORETIC ANALYSIS, AND MODECHART......Page 174
6.2 EVENT- ACTION MODEL......Page 175
6.3 REAL- TIME LOGIC......Page 176
6.4 RESTRICTED RTL FORMULAS......Page 178
6.5 CHECKING FOR UNSATISFIABILITY......Page 181
6.6 EFFICIENT UNSATISFIABILITY CHECK......Page 183
6.6.1 Analysis Complexity and Optimization......Page 186
6.7 INDUSTRIAL EXAMPLE: NASA X- 38 CREW RETURN VEHICLE......Page 187
6.7.2 Timing Properties......Page 188
6.7.4 RTL Specification......Page 189
6.7.5 RTL Representation Converted to Presburger Arithmetic......Page 194
6.7.6 Constraint Graph Analysis......Page 197
6.8.1 Modes......Page 198
6.8.2 Transitions......Page 200
6.9.1 System Computations......Page 201
6.9.3 Timing Properties......Page 202
6.9.4 Minimum and Maximum Distance Between Endpoints......Page 204
6.9.5 Exclusion and Inclusion of Endpoint and Interval......Page 205
6.11 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 206
6.12 SUMMARY......Page 207
EXERCISES......Page 209
7.1 LYNCH– VAANDRAGER AUTOMATA- THEORETIC APPROACH......Page 213
7.1.1 Timed Executions......Page 214
7.1.2 Timed Traces......Page 215
7.1.4 MMT Automata......Page 216
7.1.5 Verification Techniques......Page 217
7.2.1 Untimed Traces......Page 219
7.2.2 Timed Traces......Page 220
7.2.3 Alur– Dill Timed Automata......Page 224
7.3.1 Clock Regions......Page 227
7.3.2 Region Automaton......Page 229
7.3.3 Verification Algorithm......Page 230
7.4 AVAILABLE TOOLS......Page 231
7.6 SUMMARY......Page 233
EXERCISES......Page 236
8.1 UNTIMED PETRI NETS......Page 238
8.2 PETRI NETS WITH TIME EXTENSIONS......Page 240
8.2.2 Time Petri Nets......Page 241
8.2.3 High- Level Timed Petri Nets......Page 244
8.3 TIME ER NETS......Page 246
8.3.1 Strong and Weak Time Models......Page 249
8.4 PROPERTIES OF HIGH- LEVEL PETRI NETS......Page 250
8.5 BERTHOMIEU– DIAZ ANALYSIS ALGORITHM FOR TPNS......Page 252
8.5.1 Determining Fireability of Transitions from Classes......Page 253
8.6 MILANO GROUP’S APPROACH TO HLTPN ANALYSIS......Page 255
8.6.1 Facilitating Analysis with TRIO......Page 256
8.7 PRACTICALITY: AVAILABLE TOOLS......Page 257
8.8 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 258
8.9 SUMMARY......Page 259
EXERCISES......Page 262
9.1 UNTIMED PROCESS ALGEBRAS......Page 263
9.2 MILNER’S CALCULUS OF COMMUNICATING SYSTEMS......Page 264
9.2.1 Direct Equivalence of Behavior Programs......Page 265
9.2.2 Congruence of Behavior Programs......Page 266
9.3 TIMED PROCESS ALGEBRAS......Page 267
9.4 ALGEBRA OF COMMUNICATING SHARED RESOURCES......Page 268
9.4.2 Semantics of ACSR: Operational Rules......Page 269
9.4.3 Example Airport Radar System......Page 274
9.5 ANALYSIS AND VERIFICATION......Page 276
9.5.1 Analysis Example......Page 278
9.5.2 Using VERSA......Page 279
9.5.3 Practicality......Page 280
9.7 AVAILABLE TOOLS......Page 281
9.9 SUMMARY......Page 282
EXERCISES......Page 284
DESIGN AND ANALYSIS OF PROPOSITIONAL- LOGIC RULE- BASED SYSTEMS......Page 285
10.1 REAL- TIME DECISION SYSTEMS......Page 286
10.2 REAL- TIME EXPERT SYSTEMS......Page 288
THE EQL LANGUAGE......Page 289
10.3.4 The INPUTVAR Declaration......Page 290
10.3.6 The RULES Section......Page 291
10.3.7 The Output Section......Page 293
10.4 STATE- SPACE REPRESENTATION......Page 295
10.5 COMPUTER- AIDED DESIGN TOOLS......Page 298
10.5.1 Analysis Example......Page 301
10.6 THE ANALYSIS PROBLEM......Page 306
10.6.1 Finite Domains......Page 307
10.6.2 Special Form: Compatible Assignment to Constants,......Page 309
10.6.3 The General Analysis Strategy......Page 310
CONTROL SYSTEM......Page 312
10.8 THE SYNTHESIS PROBLEM......Page 320
Rule- Based Programs......Page 323
Time- Budgeting Problem......Page 324
10.9 SPECIFYING TERMINATION CONDITIONS IN ESTELLA......Page 327
10.9.1 Overview of the Analysis Methodology......Page 328
10.9.2 Facility for Specifying Behavioral Constraint Assertions......Page 330
10.9.3 Context- Free Grammar for Estella......Page 339
10.10 TWO INDUSTRIAL EXAMPLES......Page 343
the ISA Expert System......Page 344
Meta Rules of the Fuel Cell Expert System......Page 346
10.11.1 General Analysis Algorithm......Page 350
10.11.2 Selecting Independent Rule Sets......Page 351
10.11.3 Checking Compatibility Conditions......Page 356
10.11.4 Checking Cycle- Breaking Conditions......Page 357
10.12 QUANTITATIVE TIMING ANALYSIS ALGORITHMS......Page 359
10.12.1 Overview......Page 360
10.12.2 The Equational Logic Language......Page 361
10.12.4 High- Level Dependency Graph......Page 363
10.12.5 Program Execution and Response Time......Page 365
10.12.7 Response- Time Analysis Problem and Special Form......Page 367
10.12.9 Special Form A......Page 368
10.12.10 Special Form D and Algorithm D......Page 370
10.12.11 The General Analysis Algorithm......Page 378
10.12.12 Proofs......Page 380
10.13 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 386
10.14 SUMMARY......Page 389
EXERCISES......Page 391
TIMING ANALYSIS OF PREDICATE- LOGIC RULE- BASED SYSTEMS......Page 393
11.1.1 Overview......Page 395
11.1.2 The Rete Network......Page 398
11.2.1 Static Analysis of Control Paths in OPS5......Page 399
11.2.2 Termination Analysis......Page 401
11.2.3 Timing Analysis......Page 414
11.2.4 Static Analysis......Page 415
11.2.5 WM Generation......Page 419
11.2.6 Implementation and Experiment......Page 423
11.3 CHENG– CHEN TIMING ANALYSIS METHODOLOGY......Page 425
11.3.1 Introduction......Page 426
11.3.2 Classification of OPS5 Programs......Page 427
11.3.3 Response Time of OPS5 Systems......Page 431
11.3.4 List of Symbols......Page 447
11.3.5 Experimental Results......Page 448
11.3.6 Removing Cycles with the Help of the Programmer......Page 449
11.4 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 456
11.5 SUMMARY......Page 458
EXERCISES......Page 461
OPTIMIZATION OF RULE- BASED SYSTEMS......Page 462
12.1 INTRODUCTION......Page 463
12.2 BACKGROUND......Page 464
12.3 BASIC DEFINITIONS......Page 465
12.3.1 EQL Program......Page 466
on an EQL Program Paradigm......Page 467
12.3.3 State- Space Representation......Page 468
12.3.4 Derivation of Fixed Points......Page 470
12.4.1 Decomposition of an EQL( B) Program......Page 471
12.4.2 Derivation of an Optimized State- Space Graph......Page 473
12.4.3 Synthesis of an Optimized EQL( B) Program......Page 480
12.5 EXPERIMENTAL EVALUATION......Page 481
12.5.1 EQL( B) Programs without Cycles......Page 482
12.5.2 EQL( B) Programs with Cycles......Page 483
Assessment Expert System......Page 484
12.6.1 Qualitative Comparison of Optimization Methods......Page 486
by Optimization Algorithms......Page 487
12.7 HISTORICAL PERSPECTIVE AND RELATED WORK......Page 488
12.8 SUMMARY......Page 490
EXERCISES......Page 491
BIBLIOGRAPHY......Page 493
INDEX......Page 531