This book constitutes the refereed proceedings of the 11th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2009, and 29th IFIP WG 6.1 Formal Techniques for Networked and Distributed Systems, FORTE 2009, held in Lisboa, Portugal, in June 2009. The 12 revised full papers presented together with 6 short papers were carefully reviewed and selected from 42 submissions. The papers cover topics such as formal verification, algorithms and implementations, modeling and testing, process algebra and calculus as well as analysis of distributed systems.
Author(s): David Lee, Antonia Lopes, Arnd Poetzsch-Heffter
Edition: 1
Year: 2009
Language: English
Pages: 249
front-matter.pdf......Page 1
Introduction......Page 11
Site Calls......Page 12
Combinators......Page 13
Definitions......Page 14
Functional Core Language......Page 15
Translating Cor to Orc......Page 18
Integrating Cor and Orc......Page 19
Site Library......Page 21
Function Library......Page 22
Fork-Join......Page 23
Sequential Fork-Join......Page 24
Parallel Or......Page 25
Timeout......Page 26
Fold......Page 27
Routing......Page 28
Larger Examples......Page 30
Conclusion......Page 34
References......Page 35
Introduction......Page 36
ALBERT in a Nutshell......Page 37
ALBERT's Operational Semantics......Page 39
ALBERT's Semantics Automata......Page 40
From ALBERT to ASA......Page 41
Towards an Efficient Implementation......Page 43
A Formal Model for an Efficient Implementation......Page 44
Experimental Evaluation......Page 46
Related Work......Page 48
Conclusions......Page 49
References......Page 50
Introduction......Page 51
Model......Page 54
Exact Context-Sensitive Symbolic Analysis......Page 55
Approximated Context-Sensitive Symbolic Algorithm......Page 58
Computing Predecessors......Page 59
Experimental Results......Page 61
Conclusions and Related Work......Page 63
References......Page 64
Introduction......Page 67
Parameterized Systems......Page 69
Abstract Domains for Parameterized Systems......Page 71
Backward-Reachability Analysis......Page 74
Enforcing Convergence......Page 78
Conclusion......Page 80
References......Page 81
Introduction......Page 83
Background......Page 85
Transformation Principle......Page 86
Transformation Function......Page 87
Consistency Criteria......Page 88
Operational Transformation Algorithms......Page 89
UPPAAL's Model......Page 90
Modelling Execution Environment of OT Algorithms......Page 91
Verification of the Convergence Property......Page 94
Related Work......Page 96
Conclusion......Page 97
References......Page 98
Introduction......Page 100
Definition of a Recursive Parametric FSA......Page 101
RP-FSA and $\epsilon$-Removal......Page 102
Preliminaries......Page 105
Proving the Sufficient Condition......Page 109
Proving the Necessary Condition......Page 113
References......Page 114
Introduction......Page 116
TiMo......Page 117
MobileCalculi Framework......Page 119
Software Framework for TiMo......Page 122
Implementation Soundness......Page 123
Example......Page 127
References......Page 130
Introduction......Page 132
CARRIOCAS Project......Page 133
Path Computation Element Communication Protocol......Page 134
IF Toolset......Page 136
Overall Architecture......Page 137
States, Internal Variables, and Timers......Page 138
Remarks......Page 139
Validation with IF Observers......Page 141
Validation Results......Page 142
Remarks......Page 143
Test Generation and Results......Page 144
Conclusions......Page 145
References......Page 146
Introduction......Page 147
Preliminaries......Page 149
Separability Relation and Separating Sequences......Page 153
R-Distinguishability Relation and $r$-Distinguishing Sets......Page 156
Conclusion and Further Research Work......Page 159
References......Page 160
Introduction......Page 162
General Approach......Page 163
System Model and Its Formalization......Page 166
Concrete Syntax and Derivation of Abstract Syntax......Page 169
Semantic Mapping and Its Formalization......Page 171
Example: Cyclic Inheritance Problem......Page 172
Related Work......Page 173
Conclusion and Future Work......Page 174
References......Page 175
Introduction......Page 177
Assemblages in Dream......Page 178
Calculus......Page 180
Type System......Page 182
Discussion......Page 186
Type Inference and Its Implementation......Page 187
Related Work......Page 188
Conclusion......Page 189
References......Page 190
Introduction......Page 192
Syntax......Page 193
Semantics......Page 195
Equivalences......Page 196
Syntax......Page 198
Semantics......Page 199
Privacy in Electronic Voting Protocols......Page 202
Related and Future Work......Page 205
References......Page 206
Introduction......Page 208
Syntax......Page 211
Semantics......Page 213
Proof Methods and Methodology......Page 214
Applying the Methodology to the Case Study......Page 215
Encoding the Case Study......Page 216
Weak Bisimulation Relations via Invariants......Page 219
Conclusion and Future Work......Page 221
References......Page 222
Introduction......Page 223
Equation Solving in the Logic Context......Page 224
Submodule Construction for Synchronous Systems and LTS......Page 226
Submodule Construction for Interleaving Semantics......Page 227
References......Page 228
Specifying Service Composition with SRML......Page 229
Specifying Service Interfaces with SRML......Page 230
Encoding Service Composition with State Machines......Page 232
Model-Checking Service Modules: The TravelBooking Example......Page 233
References......Page 234
Introduction......Page 235
The Modeling Language Creol......Page 236
Representation of a Run......Page 237
Dynamic Symbolic Execution of Distributed Objects......Page 238
Application to Testing......Page 239
References......Page 240
Introduction......Page 241
Formal Model......Page 242
References......Page 246
Introduction......Page 247
Creating the Type Graph......Page 248
Constructing Syntax Graphs from Code......Page 250
Conclusion and Future Work......Page 251
References......Page 252
Introduction......Page 253
AODV Protocol and Its Simulator......Page 254
Metamorphic Testing on AODV Simulator......Page 255
Conclusion......Page 257
References......Page 258
back-matter.pdf......Page 259
