A Process Algebraic Approach to Software Architecture Design

by Aldini, Alessandro; Bernardo, Marco; Corradini, Flavio

• ISBN13: 9781848002227
• ISBN10: 184800222X
• Format: Hardcover
• Copyright: 2009-11-30
• Publisher: Springer-Nature New York Inc

Summary

The design and the verification of modern software applications requires the analysis of several different aspects, such as software correctness, quality of service, and security, and of the possible inter-relations among them. Process algebraic architectural languages and the related analysis techniques provide a formal paradigm that allows for the modeling and analysis of such systems and of the related properties during the early stages of the design process. The book presents such a paradigm in a novel way that privileges the discussion of its foundational characteristics and then introduces a number of guidelines, integrated with ad-hoc methodologies and exemplifying case studies, to support the practical benefits of using such a paradigm. The book can be of help for both researchers and graduate students who intend to approach the process algebraic formal paradigm and for the practitioners who intend to apply the related approach to software design and verification.

Table of Contents

Process Calculi and Behavioral Equivalences
Process Algebra	p. 3
Concurrency, Communication, and Nondeterminism	p. 3
Running Example: Producer-Consumer System	p. 7
PC: Process Calculus for Nondeterministic Processes	p. 7
Syntax: Actions and Behavioral Operators	p. 8
Semantics: Structural Operational Rules	p. 10
Bisimulation Equivalence	p. 13
Equivalence Relations and Preorders	p. 13
Definition of the Behavioral Equivalence	p. 14
Conditions and Characterizations	p. 16
Congruence Property	p. 16
Sound and Complete Axiomatization	p. 17
Modal Logic Characterization	p. 18
Verification Algorithm	p. 19
Abstracting from Invisible Actions	p. 19
Testing Equivalence	p. 23
Definition of the Behavioral Equivalence	p. 23
Conditions and Characterizations	p. 24
Congruence Property	p. 27
Sound and Complete Axiomatization	p. 28
Modal Logic Characterization	p. 29
Verification Algorithm	p. 30
Trace Equivalence	p. 31
Definition of the Behavioral Equivalence	p. 32
Congruence Property	p. 32
Sound and Complete Axiomatization	p. 33
Modal Logic Characterization	p. 33
Verification Algorithm	p. 34
The Linear-Time/Branching-Time Spectrum	p. 35
Deterministically Timed Process Algebra	p. 41
Concurrency, Communication, and Deterministic Time	p. 41
Deterministically Timed Process Calculi	p. 43
TPC: Timed Process Calculus with Durationless Actions	p. 43
DPC: Timed Process Calculus with Durational Actions	p. 46
Deterministically Timed Behavioral Equivalences	p. 50
Definition of Timed Bisimulation Equivalence	p. 51
Congruence Property	p. 52
Sound and Complete Axiomatization	p. 53
Modal Logic Characterization	p. 53
Verification Algorithm	p. 55
Durational Bisimulation Equivalence and its Properties	p. 55
Semantics-Preserving Mapping for Eagerness	p. 57
Differences Between TPC and DPC	p. 57
From DPC to TPC Under Eagerness	p. 58
Semantics-Preserving Mapping for Laziness	p. 59
Lazy TPC	p. 59
Lazy DPC	p. 60
From DPC to TPC Under Laziness	p. 63
Semantics-Preserving Mapping for Maximal Progress	p. 63
Maximal Progress TPC	p. 64
Maximal Progress DPC	p. 64
From DPC to TPC Under Maximal Progress	p. 67
Expressiveness of Eagerness, Laziness, Maximal Progress	p. 67
Synchronization Issues	p. 68
Choosing at Different Times	p. 70
Performing Infinitely Many Actions at the Same Time	p. 71
Performing Finitely Many Actions at the Same Time	p. 72
Coincidence Result for Sequential Processes	p. 73
Stochastically Timed Process Algebra	p. 75
Concurrency, Communication, and Stochastic Time	p. 75
MPC: Markovian Process Calculus with Durational Actions	p. 78
Markov Chains	p. 78
Syntax and Semantics	p. 80
Markovian Bisimulation Equivalence	p. 84
Exit Rates and Exit Probabilities	p. 85
Definition of the Behavioral Equivalence	p. 86
Conditions and Characterizations	p. 88
Congruence Property	p. 89
Sound and Complete Axiomatization	p. 90
Modal Logic Characterization	p. 91
Verification Algorithm	p. 92
Abstracting from Invisible Actions with Zero Duration	p. 93
Markovian Testing Equivalence	p. 99
Probability and Duration of Computations	p. 99
Definition of the Behavioral Equivalence	p. 101
Conditions and Characterizations	p. 103
Congruence Property	p. 108
Sound and Complete Axiomatization	p. 109
Modal Logic Characterization	p. 110
Verification Algorithm	p. 112
Markovian Trace Equivalence	p. 114
Definition of the Behavioral Equivalence	p. 114
Conditions and Characterizations	p. 116
Congruence Property	p. 117
Sound and Complete Axiomatization	p. 117
Modal Logic Characterization	p. 118
Verification Algorithm	p. 119
Exactness of Markovian Behavioral Equivalences	p. 120
The Markovian Linear-Time/Branching-Time Spectrum	p. 121
Process Algebra for Software Architecture
Component-Oriented Modeling	p. 127
Software Architecture Description Languages	p. 127
Running Example: Client-Server System	p. 129
Architectural Upgrade of Process Algebra: Guidelines	p. 129
G1: Separating Behavior and Topology Descriptions	p. 129
G2: Reusing Component and Connector Specification	p. 129
G3: Eliciting Component and Connector Interface	p. 130
G4: Classifying Communication Synchronicity	p. 131
G5: Classifying Communication Multiplicity	p. 132
G6: Textual and Graphical Notations (PADL Syntax)	p. 133
G7: Dynamic and Static Operators	p. 135
Translation Semantics for PADL	p. 138
Semantics of Individual Elements	p. 139
Semantics of Interacting Elements	p. 144
Summarizing Example: Pipe-Filter System	p. 147
G8: Supporting Architectural Styles	p. 152
Architectural Types	p. 153
Hierarchical Modeling	p. 154
Behavioral Conformity	p. 156
Exogenous Variations	p. 158
Endogenous Variations	p. 160
Multiplicity Variations	p. 163
Comparisons	p. 164
Comparison with Process Algebra	p. 164
Comparison with Parallel Composition Operators	p. 165
Comparison with Other Software Architecture Languages	p. 166
Component-Oriented Functional Verification	p. 169
Mismdet: Architecture-Level Mismatch Detection	p. 169
Class of Properties and Detection Strategy	p. 170
Architectural Compatibility of Star-Shaped Topologies	p. 173
Case Study: Compressing Proxy System	p. 174
Architectural Interoperability of Cycle-Shaped Topologies	p. 179
Case Study: Cruise Control System	p. 183
Generalization to Arbitrary Topologies	p. 188
Case Study: Simulator for the Cruise Control System	p. 190
Generalization to Architectural Types	p. 193
Generalization to Internal Behavioral Variations	p. 193
Generalization to Exogenous Variations	p. 194
Generalization to Endogenous Variations	p. 197
Generalization to Multiplicity Variations	p. 199
Comparisons	p. 199
Component-Oriented Performance Evaluation	p. 203
Perfsel: Performance-Driven Architectural Selection	p. 203
Class of Measures and Selection Strategy	p. 205
Emilia: Extending PADL with Performance Aspects	p. 208
Queueing Systems and Queueing Networks	p. 211
From ÆEmilia Descriptions to Queueing Networks	p. 216
General Syntactical Restrictions	p. 217
Queueing Network Basic Elements	p. 218
Documental Functions	p. 223
Characterizing Functions	p. 223
Case Study: Selecting Compiler Architectures	p. 225
Sequential Architecture	p. 225
Pipeline Architecture	p. 229
Concurrent Architecture	p. 234
Scenario-Based Performance Selection	p. 236
Comparisons	p. 238
Trading Dependability and Performance	p. 239
DepPerf: Mixed View of Dependability and Performance	p. 239
Running Example: Multilevel Security Routing System	p. 242
First Phase of DepPerf: Noninterference Analysis	p. 244
Noninterference Theory	p. 245
Noninterference Verification	p. 246
Component-Oriented Noninterference Check	p. 249
Interpretation and Feedback	p. 252
Second Phase of DepPerf: Performance Evaluation	p. 255
Model Validation	p. 256
Analysis and Tuning	p. 256
Measure Specification Language	p. 258
Case Study I: The Network NRL Pump	p. 260
Informal Specification	p. 260
Architectural Description	p. 262
Noninterference Analysis	p. 267
Performance Evaluation	p. 272
Case Study II: Power-Manageable System	p. 276
Informal Specification	p. 276
Architectural Description	p. 278
Noninterference Analysis	p. 281
Performance Evaluation	p. 284
Comparisons	p. 287
References	p. 291
Index	p. 301
Table of Contents provided by Ingram. All Rights Reserved.