Concurrency Theory (eBook)

Calculi an Automata for Modelling Untimed and Timed Concurrent Systems

Howard Bowman, Rodolfo Gomez (Autoren)

eBook Download: PDF

2006 | 2006
XX, 422 Seiten
Springer London (Verlag)
978-1-84628-336-9 (ISBN)

Infos

Intheworldweliveinconcurrencyisthenorm.Forexample,thehumanbody isamassivelyconcurrentsystem,comprisingahugenumberofcells,allsim- taneously evolving and independently engaging in their individual biological processing.Inaddition,inthebiologicalworld,trulysequentialsystemsrarely arise. However, they are more common when manmade artefacts are cons- ered. In particular, computer systems are often developed from a sequential perspective. Why is this? The simple reason is that it is easier for us to think about sequential, rather than concurrent, systems. Thus, we use sequentiality as a device to simplify the design process. However, the need for increasingly powerful, ?exible and usable computer systems mitigates against simplifying sequentiality assumptions. A good - ample of this is the all-powerful position held by the Internet, which is highly concurrent at many di?erent levels of decomposition. Thus, the modern c- puter scientist (and indeed the modern scientist in general) is forced to think aboutconcurrentsystemsandthesubtleandintricatebehaviourthatemerges from the interaction of simultaneously evolving components. Over a period of 25 years, or so, the ?eld of concurrency theory has been involved in the development of a set of mathematical techniques that can help system developers to think about and build concurrent systems. These theories are the subject matter of this book.

Inhalt

Preface 6
Contents 17
Part I Introduction 23
1 Background on Concurrency Theory 24
1.1 Concurrency Is Everywhere 24
1.2 Characteristics of Concurrent Systems 25
1.3 Classes of Concurrent Systems 27
1.3.1 Basic Event Ordering 27
1.3.2 Timing Axis 28
1.3.3 Probabilistic Choice Axis 29
1.3.4 Mobility Axis 30
1.4 Mathematical Theories 30
1.5 Overview of Book 34
Part II Concurrency Theory – Untimed Models 35
2 Process Calculi: LOTOS 37
2.1 Introduction 37
2.2 Example Specifications 38
2.2.1 A Communication Protocol 38
2.2.2 The Dining Philosophers 40
2.3 Primitive Basic LOTOS 40
2.3.1 Abstract Actions 44
2.3.2 Action Prefix 46
2.3.3 Choice 47
2.3.4 Nondeterminism 48
2.3.5 Process Definition 52
2.3.6 Concurrency 59
2.3.6.1 Independent Parallelism 59
2.3.6.2 General Form 61
2.3.6.3 Example 64
2.3.6.4 Why Synchronous Communication? 64
2.3.7 Sequential Composition and Exit 65
2.3.8 Syntax of pbLOTOS 68
2.4 Example 70
3 Basic Interleaved Semantic Models 73
3.1 A General Perspective on Semantics 73
3.1.1 Why Semantics? 73
3.1.2 Formal Definition 75
3.1.3 Modelling Recursion 79
3.1.4 What Makes a Good Semantics? 81
3.2 Trace Semantics 81
3.2.1 The Basic Approach 81
3.2.2 Formal Semantics 84
3.2.2.1 Preliminaries: Traces 84
3.2.2.2 A Denotational Trace Semantics for pbLOTOS 85
3.2.3 Development Relations 91
3.2.3.1 Trace Preorder 91
3.2.3.2 Trace Equivalence 93
3.2.4 Discussion 93
3.3 Labelled Transition Systems 94
3.3.1 The Basic Approach 94
3.3.2 Formal Semantics 96
3.3.2.1 Preliminaries: Labelled Transition Systems 96
3.3.2.2 An Operational Semantics for LOTOS 97
3.3.2.3 Deriving Trace Semantics from Labelled Transition Systems 102
3.3.3 Development Relations 103
3.3.3.1 Basic Equivalence Relations 103
3.3.3.2 Refinement Relations and Induced Equivalences 114
3.4 Verification Tools 119
3.4.1 Overview of CADP 120
3.4.2 Bisimulation Checking in CADP 121
4 True Concurrency Models: Event Structures 123
4.1 Introduction 123
4.2 The Basic Approach – Event Structures 125
4.3 Event Structures and pbLOTOS 130
4.4 An Event Structures Semantics for pbLOTOS 133
4.5 Relating Event Structures to Labelled Transition Systems 141
4.6 Development Relations 144
4.7 Alternative Event Structure Models 152
4.8 Summary and Discussion 156
5 Testing Theory and the Linear Time – Branching Time Spectrum 158
5.1 Trace-refusals Semantics 158
5.1.1 Introduction 158
5.1.2 The Basic Approach 160
5.1.2.1 Example 1 161
5.1.2.2 Example 2 161
5.1.2.3 Example 3 161
5.1.2.4 Example 4 162
5.1.3 Deriving Trace-refusal Pairs 162
5.1.3.1 Deriving Trace-refusals from Labelled Transition Systems 162
5.1.3.2 Direct Denotational Semantics 163
5.1.4 Internal Behaviour 163
5.1.5 Development Relations: Equivalences 169
5.1.6 Nonequivalence Development Relations 171
5.1.6.1 Conformance 171
5.1.6.2 Reduction 173
5.1.6.3 Extension 174
5.1.7 Explorations of Congruence 175
5.1.8 Summary and Discussion 176
5.2 Testing Justification for Trace-refusals Semantics 177
5.3 Testing Theory in General and the Linear Time – Branching Time Spectrum 178
5.3.1 Sequence-based Testing 179
5.3.2 Tree-based Testing 180
5.4 Applications of Trace-refusals Relations in Distributed Systems 183
5.4.1 Relating OO Concepts to LOTOS 183
5.4.2 Behavioural Subtyping 184
5.4.2.1 Relating LOTOS Relations and Subtyping 186
5.4.2.2 Functionality Extension and Undefined 188
5.4.2.3 Adding Unde.nedness to LOTOS Specifications 192
5.4.3 Viewpoints and Consistency 194
5.4.3.1 Consistency Definition 195
5.4.3.2 Consistency in LOTOS 197
5.4.3.3 Discussion 197
Part III Concurrency Theory – Further Untimed Notations 198
6 Beyond pbLOTOS 200
6.1 Basic LOTOS 200
6.1.1 Disabling 200
6.1.2 Generalised Choice 203
6.1.3 Generalised Parallelism 204
6.1.4 Verbose Specification Syntax 205
6.1.5 Verbose Process Syntax 205
6.1.6 Syntax of bLOTOS 206
6.2 Full LOTOS 207
6.2.1 Guarded Choice 208
6.2.2 Specification Notation 208
6.2.3 Process Definition and Invocation 209
6.2.4 Value Passing Actions 209
6.2.4.1 Value Passing and Synchronisation 212
6.2.4.2 Value Passing and Internal Behaviour 213
6.2.4.3 Illustration of Value Passing 215
6.2.5 Local Definitions 217
6.2.6 Selection Predicates 217
6.2.7 Generalised Choice 218
6.2.8 Parameterised Enabling 219
6.2.9 Syntax of fLOTOS 221
6.2.10 Comments 221
6.3 Examples 222
6.3.1 Communication Protocol 222
6.3.2 Dining Philosophers 225
6.4 Extended LOTOS 228
7 Comparison of LOTOS with CCS and CSP 230
7.1 CCS and LOTOS 232
7.1.1 Parallel Composition and Complementation of Actions 232
7.1.2 Restriction and Hiding 235
7.1.3 Internal Behaviour 236
7.1.4 Minor Di.erences 236
7.2 CSP and LOTOS 237
7.2.1 Alphabets 237
7.2.2 Internal Actions 239
7.2.3 Choice 240
7.2.3.1 Deterministic Choice (also Called Guarded Alternative) 240
7.2.3.2 External Choice 241
7.2.3.3 Nondeterministic Choice 241
7.2.4 Parallelism 242
7.2.5 Hiding 242
7.2.6 Comparison of LOTOS Trace-refusals with CSP Failures-divergences 243
7.2.6.1 Divergence 243
7.2.6.2 Development Relations and Congruence 245
8 Communicating Automata 248
8.1 Introduction 248
8.2 Networks of Communicating Automata 249
8.2.1 Component Automata 249
8.2.2 Parallel Composition 251
8.2.2.1 Basic Notation 251
8.2.2.2 Formal Definition 252
8.2.3 Example Specifications 254
8.2.4 Semantics and Development Relations 255
8.2.5 Verification of Networks of Communicating Automata 256
8.2.5.1 Computation Tree Logic (CTL) 256
8.2.5.2 Model-checking CTL 261
8.2.6 Relationship to Process Calculi 261
8.2.6.1 Encoding Networks of CAs into Process Calculi 261
8.2.6.2 Comparing Communicating Automata Networks and Process Calculi 263
8.3 Infinite State Communicating Automata 265
8.3.1 Networks of Infinite State Communicating Automata 266
8.3.1.1 Component Automata 266
8.3.1.2 Parallel Composition 267
8.3.2 Semantics of ISCAs as Labelled Transition Systems 269
Part IV Concurrency Theory – Timed Models 271
9 Timed Process Calculi, a LOTOS Perspective 273
9.1 Introduction 273
9.2 Timed LOTOS – The Issues 274
9.2.1 Timed Action Enabling 274
9.2.2 Urgency 279
9.2.3 Persistency 282
9.2.4 Nondeterminism 283
9.2.5 Synchronisation 284
9.2.6 Timing Domains 285
9.2.7 Time Measurement 285
9.2.8 Timing of Nonadjacent Actions 286
9.2.9 Timed Interaction Policies 287
9.2.10 Forms of Internal Urgency 288
9.2.11 Discussion 290
9.3 Timed LOTOS Notation 290
9.3.1 The Language 290
9.3.2 Example Specifications 293
9.4 Timing Anomalies in tLOTOS 295
9.5 E-LOTOS, the Timing Extensions 297
10 Semantic Models for tLOTOS 299
10.1 Branching Time Semantics 299
10.1.1 Timed Transition Systems 299
10.1.2 Operational Semantics 301
10.1.3 Branching Time Development Relations 311
10.2 True Concurrency Semantics 316
10.2.1 Introduction 316
10.2.2 Timed Bundle Event Structures 317
10.2.3 Causal Semantics for tLOTOS 320
10.2.3.1 Inaction, Successful Termination and Action Prefix 321
10.2.3.2 Delay, Hiding and Relabelling 322
10.2.3.3 Choice 324
10.2.3.4 Enabling 324
10.2.3.5 Parallel Composition 325
10.2.3.6 Process Instantiation 328
10.2.4 Anomalous Behaviour 330
10.2.5 Discussion 332
11 Timed Communicating Automata 333
11.1 Introduction 333
11.2 Timed Automata – Formal Definitions 335
11.2.1 Syntax 336
11.2.1.1 Example: A TA Specification for the Multimedia Stream 336
11.2.2 Semantics 337
11.2.2.1 Runs 340
11.2.2.2 Parallel Composition 340
11.2.2.3 A TTS Semantics for Timed Automata 342
11.2.2.4 Discussion: Urgency in Timed Automata and tLOTOS 343
11.3 Real-time Model-checking 344
11.3.1 Forward Reachability 345
11.3.1.1 Symbolic States and Operations on Zones 346
11.3.1.2 The Forward Reachability Graph 349
11.3.1.3 A Forward Reachability Algorithm 351
11.3.1.4 Difference Bound Matrices (DBMs): A Data Structure to Represent Zones 352
11.3.2 Example: Reachability Analysis on the Multimedia Stream 353
11.3.3 Issues in Real-time Model-checking 354
12 Timelocks in Timed Automata 358
12.1 Introduction 358
12.2 A Classification of Deadlocks in Timed Automata 360
12.2.1 Discussion: Justifying the Classi.cation of Deadlocks 361
12.2.2 Discussion: Timelocks in Process Calculi 362
12.3 Time-actionlocks 363
12.3.1 Timed Automata with Deadlines 364
12.3.1.1 Formal Definitions: Timed Automata with Deadlines 365
12.3.2 Example: A TAD Specification for the Multimedia Stream 369
12.4 Zeno-timelocks 370
12.4.1 Example: Zeno-timelocks in the Multimedia Stream 370
12.4.2 Nonzenoness: Syntactic Conditions 372
12.4.3 Nonzenoness: A Sufficient-and-Necessary Condition 379
12.5 Timelock Detection in Real-time Model-checkers 385
12.5.1 Uppaal 385
12.5.2 Kronos 387
13 Discrete Timed Automata 388
13.1 Infinite vs. Finite States 388
13.2 Preliminaries 391
13.2.1 Fair Transition Systems and Invariance Proofs 392
13.2.2 The Weak Monadic Second-order Theory of 1 Successor ( WS1S) and MONA 394
13.3 Discrete Timed Automata – Formal definitions 395
13.3.1 Syntax 395
13.3.2 Example: A DTA Specification for the Multimedia Stream 397
13.3.3 Semantics 398
13.4 Verifying Safety Properties over DTAs 400
13.5 Discussion: Comparing DTAs and TIOAs with Urgency 405
References 407
Appendix 418
14.1 Enabling as a Derived Operator 418
14.2 Strong Bisimulation Is a Congruence 418
14.3 Weak Bisimulation Congruence 423
14.4 Timed Enabling as a Derived Operator 428
14.5 Hiding is Not Substitutive for Timed Bisimulations 429
14.6 Substitutivity of Timed Strong Bisimulation 429
14.7 Substitutivity of Timed Rooted Weak Bisimulation 431
Index 438

Produkt-Details

• Erscheint lt. Verlag: 28.2.2006
• Zusatzinfo: XX, 422 p. 126 illus.
• Verlagsort: London
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Schlagworte: Automata • Calculus • Concurrency Theory • formal methods • Modeling • Real Time Systems • Semantics • theoretical computer science • verification
• ISBN-10: 1-84628-336-1 / 1846283361
• ISBN-13: 978-1-84628-336-9 / 9781846283369