Formal Techniques for Distributed Systems: Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE ... Programming and Software Engineering)

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. 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