Introduction / Part I: |
Background on Concurrency Theory / 1: |
Concurrency Is Everywhere / 1.1: |
Characteristics of Concurrent Systems / 1.2: |
Classes of Concurrent Systems / 1.3: |
Basic Event Ordering / 1.3.1: |
Timing Axis / 1.3.2: |
Probabilistic Choice Axis / 1.3.3: |
Mobility Axis / 1.3.4: |
Mathematical Theories / 1.4: |
Overview of Book / 1.5: |
Concurrency Theory - Untimed Models / Part II: |
Process Calculi: LOTOS / 2: |
Example Specifications / 2.1: |
A Communication Protocol / 2.2.1: |
The Dining Philosophers / 2.2.2: |
Primitive Basic LOTOS / 2.3: |
Abstract Actions / 2.3.1: |
Action Prefix / 2.3.2: |
Choice / 2.3.3: |
Nondeterminism / 2.3.4: |
Process Definition / 2.3.5: |
Concurrency / 2.3.6: |
Sequential Composition and Exit / 2.3.7: |
Syntax of pbLOTOS / 2.3.8: |
Example / 2.4: |
Basic Interleaved Semantic Models / 3: |
A General Perspective on Semantics / 3.1: |
Why Semantics? / 3.1.1: |
Formal Definition / 3.1.2: |
Modelling Recursion / 3.1.3: |
What Makes a Good Semantics? / 3.1.4: |
Trace Semantics / 3.2: |
The Basic Approach / 3.2.1: |
Formal Semantics / 3.2.2: |
Development Relations / 3.2.3: |
Discussion / 3.2.4: |
Labelled Transition Systems / 3.3: |
Verification Tools / 3.3.1: |
Overview of CADP / 3.4.1: |
Bisimulation Checking in CADP / 3.4.2: |
True Concurrency Models: Event Structures / 4: |
The Basic Approach - Event Structures / 4.1: |
Event Structures and pbLOTOS / 4.3: |
An Event Structures Semantics for pbLOTOS / 4.4: |
Relating Event Structures to Labelled Transition Systems / 4.5: |
Alternative Event Structure Models / 4.6: |
Summary and Discussion / 4.8: |
Testing Theory and the Linear Time - Branching Time Spectrum / 5: |
Trace-refusals Semantics / 5.1: |
Deriving Trace-refusal Pairs / 5.1.1: |
Internal Behaviour / 5.1.4: |
Development Relations: Equivalences / 5.1.5: |
Nonequivalence Development Relations / 5.1.6: |
Explorations of Congruence / 5.1.7: |
Testing Justification for Trace-refusals Semantics / 5.1.8: |
Testing Theory in General and the Linear Time - Branching Time Spectrum / 5.3: |
Sequence-based Testing / 5.3.1: |
Tree-based Testing / 5.3.2: |
Applications of Trace-refusals Relations in Distributed Systems / 5.4: |
Relating OO Concepts to LOTOS / 5.4.1: |
Behavioural Subtyping / 5.4.2: |
Viewpoints and Consistency / 5.4.3: |
Concurrency Theory - Further Untimed Notations / Part III: |
Beyond pbLOTOS / 6: |
Basic LOTOS / 6.1: |
Disabling / 6.1.1: |
Generalised Choice / 6.1.2: |
Generalised Parallelism / 6.1.3: |
Verbose Specification Syntax / 6.1.4: |
Verbose Process Syntax / 6.1.5: |
Syntax of bLOTOS / 6.1.6: |
Full LOTOS / 6.2: |
Guarded Choice / 6.2.1: |
Specification Notation / 6.2.2: |
Process Definition and Invocation / 6.2.3: |
Value Passing Actions / 6.2.4: |
Local Definitions / 6.2.5: |
Selection Predicates / 6.2.6: |
Parameterised Enabling / 6.2.7: |
Syntax of fLOTOS / 6.2.9: |
Comments / 6.2.10: |
Examples / 6.3: |
Communication Protocol / 6.3.1: |
Dining Philosophers / 6.3.2: |
Extended LOTOS / 6.4: |
Comparison of LOTOS with CCS and CSP / 7: |
CCS and LOTOS / 7.1: |
Parallel Composition and Complementation of Actions / 7.1.1: |
Restriction and Hiding / 7.1.2: |
Minor Differences / 7.1.3: |
CSP and LOTOS / 7.2: |
Alphabets / 7.2.1: |
Internal Actions / 7.2.2: |
Parallelism / 7.2.3: |
Hiding / 7.2.5: |
Comparison of LOTOS Trace-refusals with CSP Failures-divergences / 7.2.6: |
Communicating Automata / 8: |
Networks of Communicating Automata / 8.1: |
Component Automata / 8.2.1: |
Parallel Composition / 8.2.2: |
Semantics and Development Relations / 8.2.3: |
Verification of Networks of Communicating Automata / 8.2.5: |
Relationship to Process Calculi / 8.2.6: |
Infinite State Communicating Automata / 8.3: |
Networks of Infinite State Communicating Automata / 8.3.1: |
Semantics of ISCAs as Labelled Transition Systems / 8.3.2: |
Concurrency Theory - Timed Models / Part IV: |
Timed Process Calculi, a LOTOS Perspective / 9: |
Timed LOTOS - The Issues / 9.1: |
Timed Action Enabling / 9.2.1: |
Urgency / 9.2.2: |
Persistency / 9.2.3: |
Synchronisation / 9.2.4: |
Timing Domains / 9.2.6: |
Time Measurement / 9.2.7: |
Timing of Nonadjacent Actions / 9.2.8: |
Timed Interaction Policies / 9.2.9: |
Forms of Internal Urgency / 9.2.10: |
Timed LOTOS Notation / 9.2.11: |
The Language / 9.3.1: |
Timing Anomalies in tLOTOS / 9.3.2: |
E-LOTOS, the Timing Extensions / 9.5: |
Semantic Models for tLOTOS / 10: |
Branching Time Semantics / 10.1: |
Timed Transition Systems / 10.1.1: |
Operational Semantics / 10.1.2: |
Branching Time Development Relations / 10.1.3: |
True Concurrency Semantics / 10.2: |
Timed Bundle Event Structures / 10.2.1: |
Causal Semantics for tLOTOS / 10.2.3: |
Anomalous Behaviour / 10.2.4: |
Timed Communicating Automata / 10.2.5: |
Timed Automata - Formal Definitions / 11.1: |
Syntax / 11.2.1: |
Semantics / 11.2.2: |
Real-time Model-checking / 11.3: |
Forward Reachability / 11.3.1: |
Example: Reachability Analysis on the Multimedia Stream / 11.3.2: |
Issues in Real-time Model-checking / 11.3.3: |
Timelocks in Timed Automata / 12: |
A Classification of Deadlocks in Timed Automata / 12.1: |
Discussion: Justifying the Classification of Deadlocks / 12.2.1: |
Discussion: Timelocks in Process Calculi / 12.2.2: |
Time-actionlocks / 12.3: |
Timed Automata with Deadlines / 12.3.1: |
Example: A TAD Specification for the Multimedia Stream / 12.3.2: |
Zeno-timelocks / 12.4: |
Example: Zeno-timelocks in the Multimedia Stream / 12.4.1: |
Nonzenoness: Syntactic Conditions / 12.4.2: |
Nonzenoness: A Sufficient-and-Necessary Condition / 12.4.3: |
Timelock Detection in Real-time Model-checkers / 12.5: |
Uppaal / 12.5.1: |
Kronos / 12.5.2: |
Discrete Timed Automata / 13: |
Infinite vs. Finite States / 13.1: |
Preliminaries / 13.2: |
Fair Transition Systems and Invariance Proofs / 13.2.1: |
The Weak Monadic Second-order Theory of 1 Successor (WS1S) and MONA / 13.2.2: |
Discrete Timed Automata - Formal definitions / 13.3: |
Example: A DTA Specification for the Multimedia Stream / 13.3.1: |
Verifying Safety Properties over DTAs / 13.3.3: |
Discussion: Comparing DTAs and TIOAs with Urgency / 13.5: |
References |
Appendix |
Enabling as a Derived Operator / 14.1: |
Strong Bisimulation Is a Congruence / 14.2: |
Weak Bisimulation Congruence / 14.3: |
Timed Enabling as a Derived Operator / 14.4: |
Hiding is Not Substitutive for Timed Bisimulations / 14.5: |
Substitutivity of Timed Strong Bisimulation / 14.6: |
Substitutivity of Timed Rooted Weak Bisimulation / 14.7: |
Index |
Introduction / Part I: |
Background on Concurrency Theory / 1: |
Concurrency Is Everywhere / 1.1: |