Bowman / Gomez Concurrency Theory

Calculi an Automata for Modelling Untimed and Timed Concurrent Systems
1. Auflage 2006
ISBN: 978-1-84628-336-9
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 444 Seiten

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.

Autoren/Hrsg.

Bowman, Howard

Gomez, Rodolfo

Inhaltsverzeichnis

1;Preface;6
2;Contents;17
3;Part I Introduction;23
3.1;1 Background on Concurrency Theory;24
3.1.1;1.1 Concurrency Is Everywhere;24
3.1.2;1.2 Characteristics of Concurrent Systems;25
3.1.3;1.3 Classes of Concurrent Systems;27
3.1.3.1;1.3.1 Basic Event Ordering;27
3.1.3.2;1.3.2 Timing Axis;28
3.1.3.3;1.3.3 Probabilistic Choice Axis;29
3.1.3.4;1.3.4 Mobility Axis;30
3.1.4;1.4 Mathematical Theories;30
3.1.5;1.5 Overview of Book;34
4;Part II Concurrency Theory – Untimed Models;35
4.1;2 Process Calculi: LOTOS;37
4.1.1;2.1 Introduction;37
4.1.2;2.2 Example Specifications;38
4.1.2.1;2.2.1 A Communication Protocol;38
4.1.2.2;2.2.2 The Dining Philosophers;40
4.1.3;2.3 Primitive Basic LOTOS;40
4.1.3.1;2.3.1 Abstract Actions;44
4.1.3.2;2.3.2 Action Prefix;46
4.1.3.3;2.3.3 Choice;47
4.1.3.4;2.3.4 Nondeterminism;48
4.1.3.5;2.3.5 Process Definition;52
4.1.3.6;2.3.6 Concurrency ;59
4.1.3.6.1;2.3.6.1 Independent Parallelism;59
4.1.3.6.2;2.3.6.2 General Form;61
4.1.3.6.3;2.3.6.3 Example;64
4.1.3.6.4;2.3.6.4 Why Synchronous Communication?;64
4.1.3.7;2.3.7 Sequential Composition and Exit;65
4.1.3.8;2.3.8 Syntax of pbLOTOS;68
4.1.4;2.4 Example;70
4.2;3 Basic Interleaved Semantic Models;73
4.2.1;3.1 A General Perspective on Semantics;73
4.2.1.1;3.1.1 Why Semantics?;73
4.2.1.2;3.1.2 Formal Definition;75
4.2.1.3;3.1.3 Modelling Recursion;79
4.2.1.4;3.1.4 What Makes a Good Semantics?;81
4.2.2;3.2 Trace Semantics;81
4.2.2.1;3.2.1 The Basic Approach;81
4.2.2.2;3.2.2 Formal Semantics;84
4.2.2.2.1;3.2.2.1 Preliminaries: Traces;84
4.2.2.2.2;3.2.2.2 A Denotational Trace Semantics for pbLOTOS;85
4.2.2.3;3.2.3 Development Relations;91
4.2.2.3.1;3.2.3.1 Trace Preorder;91
4.2.2.3.2;3.2.3.2 Trace Equivalence;93
4.2.2.4;3.2.4 Discussion;93
4.2.3;3.3 Labelled Transition Systems;94
4.2.3.1;3.3.1 The Basic Approach;94
4.2.3.2;3.3.2 Formal Semantics;96
4.2.3.2.1;3.3.2.1 Preliminaries: Labelled Transition Systems;96
4.2.3.2.2;3.3.2.2 An Operational Semantics for LOTOS;97
4.2.3.2.3;3.3.2.3 Deriving Trace Semantics from Labelled Transition Systems;102
4.2.3.3;3.3.3 Development Relations ;103
4.2.3.3.1;3.3.3.1 Basic Equivalence Relations;103
4.2.3.3.2;3.3.3.2 Refinement Relations and Induced Equivalences;114
4.2.4;3.4 Verification Tools;119
4.2.4.1;3.4.1 Overview of CADP;120
4.2.4.2;3.4.2 Bisimulation Checking in CADP;121
4.3;4 True Concurrency Models: Event Structures;123
4.3.1;4.1 Introduction;123
4.3.2;4.2 The Basic Approach – Event Structures;125
4.3.3;4.3 Event Structures and pbLOTOS;130
4.3.4;4.4 An Event Structures Semantics for pbLOTOS;133
4.3.5;4.5 Relating Event Structures to Labelled Transition Systems;141
4.3.6;4.6 Development Relations;144
4.3.7;4.7 Alternative Event Structure Models;152
4.3.8;4.8 Summary and Discussion;156
4.4;5 Testing Theory and the Linear Time – Branching Time Spectrum;158
4.4.1;5.1 Trace-refusals Semantics;158
4.4.1.1;5.1.1 Introduction;158
4.4.1.2;5.1.2 The Basic Approach;160
4.4.1.2.1;5.1.2.1 Example 1;161
4.4.1.2.2;5.1.2.2 Example 2;161
4.4.1.2.3;5.1.2.3 Example 3;161
4.4.1.2.4;5.1.2.4 Example 4;162
4.4.1.3;5.1.3 Deriving Trace-refusal Pairs;162
4.4.1.3.1;5.1.3.1 Deriving Trace-refusals from Labelled Transition Systems;162
4.4.1.3.2;5.1.3.2 Direct Denotational Semantics;163
4.4.1.4;5.1.4 Internal Behaviour;163
4.4.1.5;5.1.5 Development Relations: Equivalences;169
4.4.1.6;5.1.6 Nonequivalence Development Relations;171
4.4.1.6.1;5.1.6.1 Conformance;171
4.4.1.6.2;5.1.6.2 Reduction;173
4.4.1.6.3;5.1.6.3 Extension;174
4.4.1.7;5.1.7 Explorations of Congruence;175
4.4.1.8;5.1.8 Summary and Discussion;176
4.4.2;5.2 Testing Justification for Trace-refusals Semantics;177
4.4.3;5.3 Testing Theory in General and the Linear Time – Branching Time Spectrum;178
4.4.3.1;5.3.1 Sequence-based Testing;179
4.4.3.2;5.3.2 Tree-based Testing;180
4.4.4;5.4 Applications of Trace-refusals Relations in Distributed Systems;183
4.4.4.1;5.4.1 Relating OO Concepts to LOTOS;183
4.4.4.2;5.4.2 Behavioural Subtyping;184
4.4.4.2.1;5.4.2.1 Relating LOTOS Relations and Subtyping;186
4.4.4.2.2;5.4.2.2 Functionality Extension and Undefined ;188
4.4.4.2.3;5.4.2.3 Adding Unde.nedness to LOTOS Specifications;192
4.4.4.3;5.4.3 Viewpoints and Consistency;194
4.4.4.3.1;5.4.3.1 Consistency Definition;195
4.4.4.3.2;5.4.3.2 Consistency in LOTOS;197
4.4.4.3.3;5.4.3.3 Discussion;197
5;Part III Concurrency Theory – Further Untimed Notations;198
5.1;6 Beyond pbLOTOS;200
5.1.1;6.1 Basic LOTOS;200
5.1.1.1;6.1.1 Disabling;200
5.1.1.2;6.1.2 Generalised Choice;203
5.1.1.3;6.1.3 Generalised Parallelism;204
5.1.1.4;6.1.4 Verbose Specification Syntax;205
5.1.1.5;6.1.5 Verbose Process Syntax;205
5.1.1.6;6.1.6 Syntax of bLOTOS;206
5.1.2;6.2 Full LOTOS;207
5.1.2.1;6.2.1 Guarded Choice;208
5.1.2.2;6.2.2 Specification Notation;208
5.1.2.3;6.2.3 Process Definition and Invocation;209
5.1.2.4;6.2.4 Value Passing Actions;209
5.1.2.4.1;6.2.4.1 Value Passing and Synchronisation;212
5.1.2.4.2;6.2.4.2 Value Passing and Internal Behaviour;213
5.1.2.4.3;6.2.4.3 Illustration of Value Passing;215
5.1.2.5;6.2.5 Local Definitions;217
5.1.2.6;6.2.6 Selection Predicates;217
5.1.2.7;6.2.7 Generalised Choice;218
5.1.2.8;6.2.8 Parameterised Enabling;219
5.1.2.9;6.2.9 Syntax of fLOTOS;221
5.1.2.10;6.2.10 Comments;221
5.1.3;6.3 Examples;222
5.1.3.1;6.3.1 Communication Protocol;222
5.1.3.2;6.3.2 Dining Philosophers;225
5.1.4;6.4 Extended LOTOS;228
5.2;7 Comparison of LOTOS with CCS and CSP;230
5.2.1;7.1 CCS and LOTOS;232
5.2.1.1;7.1.1 Parallel Composition and Complementation of Actions;232
5.2.1.2;7.1.2 Restriction and Hiding;235
5.2.1.3;7.1.3 Internal Behaviour;236
5.2.1.4;7.1.4 Minor Di.erences;236
5.2.2;7.2 CSP and LOTOS;237
5.2.2.1;7.2.1 Alphabets;237
5.2.2.2;7.2.2 Internal Actions;239
5.2.2.3;7.2.3 Choice;240
5.2.2.3.1;7.2.3.1 Deterministic Choice (also Called Guarded Alternative);240
5.2.2.3.2;7.2.3.2 External Choice;241
5.2.2.3.3;7.2.3.3 Nondeterministic Choice;241
5.2.2.4;7.2.4 Parallelism;242
5.2.2.5;7.2.5 Hiding;242
5.2.2.6;7.2.6 Comparison of LOTOS Trace-refusals with CSP Failures-divergences;243
5.2.2.6.1;7.2.6.1 Divergence;243
5.2.2.6.2;7.2.6.2 Development Relations and Congruence;245
5.3;8 Communicating Automata;248
5.3.1;8.1 Introduction;248
5.3.2;8.2 Networks of Communicating Automata;249
5.3.2.1;8.2.1 Component Automata;249
5.3.2.2;8.2.2 Parallel Composition ;251
5.3.2.2.1;8.2.2.1 Basic Notation;251
5.3.2.2.2;8.2.2.2 Formal Definition;252
5.3.2.3;8.2.3 Example Specifications;254
5.3.2.4;8.2.4 Semantics and Development Relations;255
5.3.2.5;8.2.5 Verification of Networks of Communicating Automata;256
5.3.2.5.1;8.2.5.1 Computation Tree Logic (CTL);256
5.3.2.5.2;8.2.5.2 Model-checking CTL;261
5.3.2.6;8.2.6 Relationship to Process Calculi ;261
5.3.2.6.1;8.2.6.1 Encoding Networks of CAs into Process Calculi;261
5.3.2.6.2;8.2.6.2 Comparing Communicating Automata Networks and Process Calculi;263
5.3.3;8.3 Infinite State Communicating Automata;265
5.3.3.1;8.3.1 Networks of Infinite State Communicating Automata;266
5.3.3.1.1;8.3.1.1 Component Automata;266
5.3.3.1.2;8.3.1.2 Parallel Composition;267
5.3.3.2;8.3.2 Semantics of ISCAs as Labelled Transition Systems;269
6;Part IV Concurrency Theory – Timed Models;271
6.1;9 Timed Process Calculi, a LOTOS Perspective;273
6.1.1;9.1 Introduction;273
6.1.2;9.2 Timed LOTOS – The Issues;274
6.1.2.1;9.2.1 Timed Action Enabling;274
6.1.2.2;9.2.2 Urgency;279
6.1.2.3;9.2.3 Persistency;282
6.1.2.4;9.2.4 Nondeterminism;283
6.1.2.5;9.2.5 Synchronisation;284
6.1.2.6;9.2.6 Timing Domains;285
6.1.2.7;9.2.7 Time Measurement;285
6.1.2.8;9.2.8 Timing of Nonadjacent Actions;286
6.1.2.9;9.2.9 Timed Interaction Policies;287
6.1.2.10;9.2.10 Forms of Internal Urgency;288
6.1.2.11;9.2.11 Discussion;290
6.1.3;9.3 Timed LOTOS Notation;290
6.1.3.1;9.3.1 The Language;290
6.1.3.2;9.3.2 Example Specifications;293
6.1.4;9.4 Timing Anomalies in tLOTOS;295
6.1.5;9.5 E-LOTOS, the Timing Extensions;297
6.2;10 Semantic Models for tLOTOS;299
6.2.1;10.1 Branching Time Semantics;299
6.2.1.1;10.1.1 Timed Transition Systems;299
6.2.1.2;10.1.2 Operational Semantics;301
6.2.1.3;10.1.3 Branching Time Development Relations;311
6.2.2;10.2 True Concurrency Semantics;316
6.2.2.1;10.2.1 Introduction;316
6.2.2.2;10.2.2 Timed Bundle Event Structures;317
6.2.2.3;10.2.3 Causal Semantics for tLOTOS;320
6.2.2.3.1;10.2.3.1 Inaction, Successful Termination and Action Prefix;321
6.2.2.3.2;10.2.3.2 Delay, Hiding and Relabelling;322
6.2.2.3.3;10.2.3.3 Choice;324
6.2.2.3.4;10.2.3.4 Enabling;324
6.2.2.3.5;10.2.3.5 Parallel Composition;325
6.2.2.3.6;10.2.3.6 Process Instantiation;328
6.2.2.4;10.2.4 Anomalous Behaviour;330
6.2.2.5;10.2.5 Discussion;332
6.3;11 Timed Communicating Automata;333
6.3.1;11.1 Introduction;333
6.3.2;11.2 Timed Automata – Formal Definitions;335
6.3.2.1;11.2.1 Syntax ;336
6.3.2.1.1;11.2.1.1 Example: A TA Specification for the Multimedia Stream;336
6.3.2.2;11.2.2 Semantics;337
6.3.2.2.1;11.2.2.1 Runs;340
6.3.2.2.2;11.2.2.2 Parallel Composition;340
6.3.2.2.3;11.2.2.3 A TTS Semantics for Timed Automata;342
6.3.2.2.4;11.2.2.4 Discussion: Urgency in Timed Automata and tLOTOS;343
6.3.3;11.3 Real-time Model-checking;344
6.3.3.1;11.3.1 Forward Reachability;345
6.3.3.1.1;11.3.1.1 Symbolic States and Operations on Zones;346
6.3.3.1.2;11.3.1.2 The Forward Reachability Graph;349
6.3.3.1.3;11.3.1.3 A Forward Reachability Algorithm;351
6.3.3.1.4;11.3.1.4 Difference Bound Matrices (DBMs): A Data Structure to Represent Zones;352
6.3.3.2;11.3.2 Example: Reachability Analysis on the Multimedia Stream;353
6.3.3.3;11.3.3 Issues in Real-time Model-checking;354
6.4;12 Timelocks in Timed Automata;358
6.4.1;12.1 Introduction;358
6.4.2;12.2 A Classification of Deadlocks in Timed Automata;360
6.4.2.1;12.2.1 Discussion: Justifying the Classi.cation of Deadlocks;361
6.4.2.2;12.2.2 Discussion: Timelocks in Process Calculi;362
6.4.3;12.3 Time-actionlocks;363
6.4.3.1;12.3.1 Timed Automata with Deadlines;364
6.4.3.1.1;12.3.1.1 Formal Definitions: Timed Automata with Deadlines;365
6.4.3.2;12.3.2 Example: A TAD Specification for the Multimedia Stream;369
6.4.4;12.4 Zeno-timelocks;370
6.4.4.1;12.4.1 Example: Zeno-timelocks in the Multimedia Stream;370
6.4.4.2;12.4.2 Nonzenoness: Syntactic Conditions;372
6.4.4.3;12.4.3 Nonzenoness: A Sufficient-and-Necessary Condition;379
6.4.5;12.5 Timelock Detection in Real-time Model-checkers;385
6.4.5.1;12.5.1 Uppaal;385
6.4.5.2;12.5.2 Kronos;387
6.5;13 Discrete Timed Automata;388
6.5.1;13.1 Infinite vs. Finite States;388
6.5.2;13.2 Preliminaries;391
6.5.2.1;13.2.1 Fair Transition Systems and Invariance Proofs;392
6.5.2.2;13.2.2 The Weak Monadic Second-order Theory of 1 Successor ( WS1S) and MONA;394
6.5.3;13.3 Discrete Timed Automata – Formal definitions;395
6.5.3.1;13.3.1 Syntax ;395
6.5.3.2;13.3.2 Example: A DTA Specification for the Multimedia Stream;397
6.5.3.3;13.3.3 Semantics;398
6.5.4;13.4 Verifying Safety Properties over DTAs;400
6.5.5;13.5 Discussion: Comparing DTAs and TIOAs with Urgency;405
7;References;407
8;Appendix;418
8.1;14.1 Enabling as a Derived Operator;418
8.2;14.2 Strong Bisimulation Is a Congruence;418
8.3;14.3 Weak Bisimulation Congruence;423
8.4;14.4 Timed Enabling as a Derived Operator;428
8.5;14.5 Hiding is Not Substitutive for Timed Bisimulations;429
8.6;14.6 Substitutivity of Timed Strong Bisimulation;429
8.7;14.7 Substitutivity of Timed Rooted Weak Bisimulation;431
9;Index;438