Part I Process Calculi and Behavioral Equivalences
1 Process Algebra .............................................. 3
1.1 Concurrency, Communication, and Nondeterminism .......... 3
1.2 Running Example: Producer-Consumer System ............... 7
1.3 PC: Process Calculus for Nondeterministic Processes ..... 7
1.3.1 Syntax: Actions and Behavioral Operators ......... 8
1.3.2 Semantics: Structural Operational Rules ......... 10
1.4 Bisimulation Equivalence ............................... 13
1.4.1 Equivalence Relations and Preorders ............. 13
1.4.2 Definition of the Behavioral Equivalence ........ 14
1.4.3 Conditions and Characterizations ................ 16
1.4.4 Congruence Property ............................. 16
1.4.5 Sound and Complete Axiomatization ............... 17
1.4.6 Modal Logic Characterization .................... 18
1.4.7 Verification Algorithm .......................... 19
1.4.8 Abstracting from Invisible Actions .............. 19
1.5 Testing Equivalence .................................... 23
1.5.1 Definition of the Behavioral Equivalence ........ 23
1.5.2 Conditions and Characterizations ................ 24
1.5.3 Congruence Property ............................. 27
1.5.4 Sound and Complete Axiomatization ............... 28
1.5.5 Modal Logic Characterization .................... 29
1.5.6 Verification Algorithm .......................... 30
1.6 Trace Equivalence ...................................... 31
1.6.1 Definition of the Behavioral Equivalence ........ 32
1.6.2 Congruence Property ............................. 32
1.6.3 Sound and Complete Axiomatization ............... 33
1.6.4 Modal Logic Characterization .................... 33
1.6.5 Verification Algorithm .......................... 34
1.7 The Linear-Time/Branching-Time Spectrum ................ 35
2 Deterministically Timed Process Algebra ..................... 41
2.1 Concurrency, Communication, and Deterministic Time ..... 41
2.2 Deterministically Timed Process Calculi ................ 43
2.2.1 TPC: Timed Process Calculus with Durationless
Actions ......................................... 43
2.2.2 DPC: Timed Process Calculus with Durational
Actions ......................................... 46
2.3 Deterministically Timed Behavioral Equivalences ........ 50
2.3.1 Definition of Timed Bisimulation Equivalence .... 51
2.3.2 Congruence Property ............................. 52
2.3.3 Sound and Complete Axiomatization ............... 53
2.3.4 Modal Logic Characterization .................... 53
2.3.5 Verification Algorithm .......................... 55
2.3.6 Durational Bisimulation Equivalence and its
Properties ...................................... 55
2.4 Semantics-Preserving Mapping for Eagerness ............. 57
2.4.1 Differences Between TPC and DPC ................. 57
2.4.2 From DPC to TPC Under Eagerness ................. 58
2.5 Semantics-Preserving Mapping for Laziness .............. 59
2.5.1 Lazy TPC ........................................ 59
2.5.2 Lazy DPC ........................................ 60
2.5.3 From DPC to TPC Under Laziness .................. 63
2.6 Semantics-Preserving Mapping for Maximal Progress ...... 63
2.6.1 Maximal Progress TPC ............................ 64
2.6.2 Maximal Progress DPC ............................ 64
2.6.3 From DPC to TPC Under Maximal Progress .......... 67
2.7 Expressiveness of Eagerness, Laziness, Maximal
Progress ............................................... 67
2.7.1 Synchronization Issues .......................... 68
2.7.2 Choosing at Different Times ..................... 70
2.7.3 Performing Infinitely Many Actions at the Same
Time ............................................ 71
2.7.4 Performing Finitely Many Actions at the Same
Time ............................................ 72
2.7.5 Coincidence Result for Sequential Processes ..... 73
3 Stochastically Timed Process Algebra ........................ 75
3.1 Concurrency, Communication, and Stochastic Time ........ 75
3.2 MPC: Markovian Process Calculus with Durational
Actions ................................................ 78
3.2.1 Markov Chains ................................... 78
3.2.2 Syntax and Semantics ............................ 80
3.3 Markovian Bisimulation Equivalence ..................... 84
3.3.1 Exit Rates and Exit Probabilities ............... 85
3.3.2 Definition of the Behavioral Equivalence ........ 86
3.3.3 Conditions and Characterizations ................ 88
3.3.4 Congruence Property ............................. 89
3.3.5 Sound and Complete Axiomatization ............... 90
3.3.6 Modal Logic Characterization .................... 91
3.3.7 Verification Algorithm .......................... 92
3.3.8 Abstracting from Invisible Actions with Zero
Duration ........................................ 93
3.4 Markovian Testing Equivalence .......................... 99
3.4.1 Probability and Duration of Computations ........ 99
3.4.2 Definition of the Behavioral Equivalence ....... 101
3.4.3 Conditions and Characterizations ............... 103
3.4.4 Congruence Property ............................ 108
3.4.5 Sound and Complete Axiomatization .............. 109
3.4.6 Modal Logic Characterization ................... 110
3.4.7 Verification Algorithm ......................... 112
3.5 Markovian Trace Equivalence ........................... 114
3.5.1 Definition of the Behavioral Equivalence ....... 114
3.5.2 Conditions and Characterizations ............... 116
3.5.3 Congruence Property ............................ 117
3.5.4 Sound and Complete Axiomatization .............. 117
3.5.5 Modal Logic Characterization ................... 118
3.5.6 Verification Algorithm ......................... 119
3.6 Exactness of Markovian Behavioral Equivalences ........ 120
3.7 The Markovian Linear-Time/Branching-Time Spectrum ..... 121
Part II Process Algebra for Software Architecture
4 Component-Oriented Modeling ................................ 127
4.1 Software Architecture Description Languages ........... 127
4.2 Running Example: Client-Server System ................. 129
4.3 Architectural Upgrade of Process Algebra:
Guidelines ............................................ 129
4.3.1 G1: Separating Behavior and Topology
Descriptions ................................... 129
4.3.2 G2: Reusing Component and Connector
Specification .................................. 129
4.3.3 G3: Eliciting Component and Connector
Interface ...................................... 130
4.3.4 G4: Classifying Communication Synchronicity .... 131
4.3.5 G5: Classifying Communication Multiplicity ..... 132
4.3.6 G6: Textual and Graphical Notations (PADL
Syntax) ........................................ 133
4.3.7 G7: Dynamic and Static Operators ............... 135
4.4 Translation Semantics for PADL ........................ 138
4.4.1 Semantics of Individual Elements ............... 139
4.4.2 Semantics of Interacting Elements .............. 144
4.5 Summarizing Example: Pipe-Filter System ............... 147
4.6 G8: Supporting Architectural Styles ................... 152
4.6.1 Architectural Types ............................ 153
4.6.2 Hierarchical Modeling .......................... 154
4.6.3 Behavioral Conformity .......................... 156
4.6.4 Exogenous Variations ........................... 158
4.6.5 Endogenous Variations .......................... 160
4.6.6 Multiplicity Variations ........................ 163
4.7 Comparisons ........................................... 164
4.7.1 Comparison with Process Algebra ................ 164
4.7.2 Comparison with Parallel Composition
Operators ...................................... 165
4.7.3 Comparison with Other Software Architecture
Languages ...................................... 166
5 Component-Oriented Functional Verification ................. 169
5.1 MlSMDET: Architecture-Level Mismatch Detection ........ 169
5.2 Class of Properties and Detection Strategy ............ 170
5.3 Architectural Compatibility of Star-Shaped
Topologies ............................................ 173
5.3.1 Case Study: Compressing Proxy System ........... 174
5.4 Architectural Interoperability of Cycle-Shaped
Topologies ............................................ 179
5.4.1 Case Study: Cruise Control System .............. 183
5.5 Generalization to Arbitrary Topologies ................ 188
5.5.1 Case Study: Simulator for the Cruise Control
System ......................................... 190
5.6 Generalization to Architectural Types ................. 193
5.6.1 Generalization to Internal Behavioral
Variations ..................................... 193
5.6.2 Generalization to Exogenous Variations ......... 194
5.6.3 Generalization to Endogenous Variations ........ 197
5.6.4 Generalization to Multiplicity Variations ...... 199
5.7 Comparisons ........................................... 199
6 Component-Oriented Performance Evaluation .................. 203
6.1 PerfSel: Performance-Driven Architectural Selection ... 203
6.2 Class of Measures and Selection Strategy .............. 205
6.3 Æmilia: Extending PADL with Performance Aspects ...... 208
6.4 Queueing Systems and Queueing Networks ................ 211
6.5 From Æmilia Descriptions to Queueing Networks ......... 216
6.5.1 General Syntactical Restrictions ............... 217
6.5.2 Queueing Network Basic Elements ................ 218
6.5.3 Documental Functions ........................... 223
6.5.4 Characterizing Functions ....................... 223
6.6 Case Study: Selecting Compiler Architectures .......... 225
6.6.1 Sequential Architecture ........................ 225
6.6.2 Pipeline Architecture .......................... 229
6.6.3 Concurrent Architecture ........................ 234
6.6.4 Scenario-Based Performance Selection ........... 236
6.7 Comparisons ........................................... 238
7 Trading Dependability and Performance ...................... 239
7.1 DepPerf: Mixed View of Dependability and
Performance ........................................... 239
7.2 Running Example: Multilevel Security Routing System ... 242
7.3 First Phase of DepPerf: Noninterference Analysis ...... 244
7.3.1 Noninterference Theory ......................... 245
7.3.2 Noninterference Verification ................... 246
7.3.3 Component-Oriented Noninterference Check ....... 249
7.3.4 Interpretation and Feedback .................... 252
7.4 Second Phase of DepPerf: Performance Evaluation ....... 255
7.4.1 Model Validation ............................... 256
7.4.2 Analysis and Tuning ............................ 256
7.4.3 Measure Specification Language ................. 258
7.5 Case Study I: The Network NRL Pump .................... 260
7.5.1 Informal Specification ......................... 260
7.5.2 Architectural Description ...................... 262
7.5.3 Noninterference Analysis ....................... 267
7.5.4 Performance Evaluation ......................... 272
7.6 Case Study II: Power-Manageable System ................ 276
7.6.1 Informal Specification ......................... 276
7.6.2 Architectural Description ...................... 278
7.6.3 Noninterference Analysis ....................... 281
7.6.4 Performance Evaluation ......................... 284
7.7 Comparisons ........................................... 287
References .................................................... 291
Index ......................................................... 301
|
