Chapter:1 Real-time system = discrete system + clock variables1
Rajeev Alur and Thomas A. Henzinger
1.1Untimed systems1
1.2Timed systems 1: safety6
1.3Timed systems 2: progress10
1.4Real-time programming15
1.5Timed systems 3: continuous environment22
1.6Analysis of timed systems27
Chapter:2 Real-time CSP31
Jim Davies and Steve Scheneider
2.1Processes31
2.2Properties40
2.3Using real-time CSP45
2.4A simple example50
2.5Case study: a distributed watchdog timer58
2.6Case study: railroad crossing69
2.7Discussion78
2.8Acknowledgments80
2.9Appendix: proof system80
Chapter:3 Visual tools for verifying real-time systems83
Jonathan Ostroff
3.1The BUILD and VERIFY tools83
3.2Modeling systems with BUILD85
3.3Correctness checking with VERIFY98
3.4Discussion100
Chapter:4 Designing supervisors for real-time systems103
Dan Ionescu
4.1Introduction103
4.2A timed temporal logic framework104
4.3Composition of TTLMs114
4.4Reachability analysis of TTLMs 117
4.5A reachability synthesis procedure119
4.6An example of supervisor design122
4.7Conclusions128
Chapter:5 Real-time symbolic model checking for discrete time models129
Sérgio V. Campos and Edmund M. Clarke
5.1Introduction129
5.2Temporal logic model checking131
5.3Binary decision diagrams132
5.4Computation tree logic133
5.5Symbolic model checking136
5.6Real-time logics138
5.7Timed transition graphs139
5.8Examples141
5.9Conclusions145
Chapter:6 Verification of an audio control protocol147
Doeko J.B. Bosscher, Indra Polak and Frits W. Vaandrager
6.1Introduction147
6.2The timed I/O automata model151
6.3Linear hybrid systems156
6.4Protocol specification160
6.5Correctness proof165
6.6Conclusions and future work169
6.7Appendix: proof of theorem 6.3.1170
Chapter:7 Approximations for verifying timing properties177
Howard Wong-Toi and David L. Dill
7.1Introduction177
7.2Fundamental approximation algorithm180
7.3Simple variations183
7.4Full approximation algorithm187
7.5Real-time systems195
7.6Approximation for timing verification197
7.7Examples199
7.8Conclusion203
Chapter:8 A Timed Full LOTOS with Time/Action Tree Semantics205
Tommaso Bolognesi and Ferdinando Lucidi
8.1Introduction205
8.2A Timed Interpretation of Full LOTOS208
8.3Adding Time-oriented Operators214
8.4Small Examples225
8.5Specification of the Tick-Tock Service229
8.6Conclusions235
Chapter:9 A Timed LOTOS extension239
Juan Quemada, Carlos Miguel Nieto, David de Frutos, and Luis Fernando Llana Díaz
9.1Introduction239
9.2The calculus240
9.3The transition system241
9.4Description of the time model243
9.5Strong bisimulation245
9.6A testing semantics248
9.7Railroad crossing example254
9.8Tick-tock case study258
9.9Conclusions263
Chapter:10 Status-oriented telephone service specification265
Bernard Stepien and Luigi Logrippo
10.1Motivation265
10.2The informal specification266
10.3Specification structure: call connection268
10.4Specification structure: call termination275
10.5Installing stations284
10.6Conclusions285
Chapter:11 Experimenting with LOTOS in the aerospace industry 287
Hubert Garavel and René-Pierre Hautbois
11.1Introduction287
11.2Airbus/340 flight warning computer290
11.3The formal description technique LOTOS293
11.4Formal description in LOTOS of the FWC294
11.5Analysis of the detailed design301
11.6Conclusion306
Chapter:12 Performance analysis and true concurrency semantics309
Ed Brinksma, Joost-Pieter Katoen, Rom Langerak and Diego Latella
12.1Introduction309
12.2The language311
12.3Timed probabilistic event structures319
12.4Semantics for timed probabilistic LOTOS326
12.5Performance analysis331
12.6Concluding remarks336
Chapter:13 State machines, temporal logic and algebraic data models 339
Armen Gabrielian
13.1Introduction339
13.2Preliminary concepts and definitions342
13.3HMS machines with algebraic objects346
13.4Hierarchical theorem proving350
13.5Feasible schedules and policy specification356
13.6Verification of a mutual exclusion protocol358
13.7Prototype HMS machine environment360
13.8Conclusions361
Chapter:14 An experiment in developing real-time systems using Mec363
Didier Bégay, Jérôme Dormoy and Patrick Félix
14.1Industrial environment363
14.2Inter-processor communication364
14.3Tools367
14.4Modeling the system369
14.5Protocol379
14.6 Testers381
14.7Results383
14.8Conclusion388
The Authors389
Bibliography399
Index421