Formal Techniques for Distributed Systems
Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 30th IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik, Island, June 6-9, 2011, Proceedings
Published on 11. June 2011
XIV, 349 pages
978-3-642-21461-5 (ISBN)
Description
This book constitutes the refereed proceedings of the 13th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2011, and the 31st IFIP WG 6.1 Formal Techniques for Networked and Distributed Systems, FORTE 2011, held in Reykjavik, Island, in June 2011, as one of the DisCoTec 2011 events. The 21 revised full papers presented together with one invited talk were carefully reviewed and selected from 65 submissions. The topics covered are formal verification, formal modeling and specification, run-time monitoring, and testing to address challenges in many different application areas, including dynamic and ad hoc networks, mobile and adaptive computation, reactive and timed systems, business processes, and distributed and concurrent systems and algorithms.
More details
Other editions
Additional editions
Roberto Bruni | Juergen Dingel
Formal Techniques for Distributed Systems
Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 30th IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik, Island, June 6-9, 2011, Proceedings
Book
05/2011
Springer
€53.49
Shipment within 7-9 days
Content
- Title Page
- Foreword
- Preface
- Organization
- Table of Contents
- On Global Types and Multi-party Sessions
- Introduction
- Global Types
- Multi-party Sessions
- Session Types
- Session Environments
- Semantic Projection
- Algorithmic Projection
- Session Subsumption
- Projection of Kleene Star
- Global Type Subsumption
- Properties of the Algorithmic Rules
- k-Exit Iterations
- Related Work
- Conclusion
- References
- Linear-Time and May-Testing in a Probabilistic Reactive Setting
- Introduction
- Background on Measure Theory
- Reactive Probabilistic Labeled Transition Systems
- rplts
- Linear-Time Semantics of rplts
- Tree-Unfolding Semantics of rplts
- May Testing for rplts
- The Sigma-Algebra of d-trees
- The May-Testing Preorder
- On the Relationship among ~ , =lin and =tree
- May-Testing and the Safety Properties of Infinite Trees
- Testing Separated rplts
- Conclusion and Related Works
- References
- A Model-Checking Tool for Families of Services
- Introduction
- Running Example: Travel Agency
- A Behavioural Model for Product Families
- Logics for MTSs
- HML+UNTIL
- Variability and Action-Based CTL: vaCTL
- Model Checking a Family of Services
- Related Work
- Conclusions and Future Work
- References
- Partial Order Methods for Statistical Model Checking and Simulation
- Introduction
- Preliminaries
- Probabilistic Automata
- Networks of PA
- PA with Variables
- Paths, Schedulers and Probabilities
- Nondeterminism in Models for Simulation
- Partial Order Techniques for Simulation
- Partial Order Reduction for PA
- Deciding Spuriousness on VPA Symbolically
- Bounded On-the-Fly Partial Order Checking
- Implementation
- Case Studies
- Binary Exponential Backoff
- Arcade Dependability Models
- Conclusion
- References
- Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking
- Introduction
- Foundations
- Stochastic Models
- Bisimulation Minimization
- SMT-Based Bounded Model Checking for Counterexample Generation
- SMT-Based and SAT-Based SBMC
- Counterexamples for MRMs
- Bisimulation Minimization
- Experimental Results
- Counterexamples for DTMCs
- Bisimulation
- Rewards
- Conclusion
- References
- Adaptable Processes (Extended Abstract)
- Introduction
- The E Calculus: Syntax, Semantics, Adaptation Problems
- Adaptable Processes, by Examples
- Bounded and Eventual Adaptation Are Undecidable in E
- The Subcalculus E- and Decidability of Bounded Adaptation
- Eventual Adaptation Is Undecidable in E-
- Concluding Remarks
- References
- A Framework for Verifying Data-Centric Protocols
- Introduction
- Distributed Computation Model of Netlog
- Data Centric Protocols
- Verifying Tree Protocols
- Spanning Tree in the Asynchronous Case
- BFS in the Synchronous Case
- Conclusion
- References
- Relational Concurrent Refinement: Timed Refinement
- Introduction
- Background
- A Partial Relational Model
- Refinement in Z
- Process Algebraic Based Refinement
- Trace Preorder
- Timed Models
- A Timed Relational Model
- A Timed Behavioural Model
- Discussion
- References
- Galois Connections for Flow Algebras
- Introduction
- Flow Algebra
- Galois Connections for Flow Algebras
- Program Graphs
- Flow Algebras over Program Graphs
- Galois Connections for Program Graphs
- Upper-Approximation of Program Graphs
- Preservation of the MOP and MFP Solutions
- Application to the Bakery Algorithm
- Conclusions
- References
- An Accurate Type System for Information Flow in Presence of Arrays
- Introduction
- Language and Semantics
- Over-Approximation of the Semantics
- A Type System for Information Flow in Arrays
- The Type System
- Example
- Properties of the Type System
- Conclusion and Future Work
- References
- Analysis of Deadlocks in Object Groups
- Introduction
- The Calculus FJg
- Syntax
- Semantics
- Deadlocks
- Contracts in FJg
- Deadlock Analysis in FJg
- Related Works
- Conclusions
- References
- Monitoring Distributed Systems Using Knowledge
- Introduction
- Preliminaries
- Knowledge Properties for Monitoring
- Building the Knowledge Table
- Monitoring Using a Knowledge Table
- Implementation and Experimental Results
- Conclusion
- References
- Global State Estimates for Distributed Systems
- Introduction
- Communicating Finite State Machines as a Model of the System
- State Estimates of Distributed Systems
- Algorithm to Compute the State Estimates
- Vector Clocks
- Computation of State Estimates
- Effective Computation of State Estimates by Means of Abstract Interpretation
- Experiments
- Conclusion and Future Work
- References
- A Process Calculus for Dynamic Networks
- Introduction
- The Process Calculus
- The Syntax
- The Semantics
- Bisimulation and Confluence
- Specification and Verification of a Leader-Election Algorithm
- The Algorithm
- Specification of the Protocol
- Verification of the Protocol
- Conclusions
- References
- On Asynchronous Session Semantics
- Introduction
- Asynchronous Network Communications in Sessions
- Syntax and Operational Semantics
- Types and Typing
- Asynchronous Session Bisimulations and Its Properties
- Labelled Transitions and Bisimilarity
- Properties of Asynchronous Session Bisimilarity
- Lauer-Needham Transform
- Discussions
- References
- Towards Verification of the Pastry Protocol Using TLA+
- Introduction
- The Join Protocol
- A First Formal Model of Pastry
- Static Model
- Dynamic Model
- Validation by Model Checking
- Correct Key Delivery
- Refining the Join Protocol
- Lease Granting Protocol
- Symmetry of Leaf Sets
- Validation
- Theorem Proving
- Conclusion and Future Work
- References
- Dynamic Soundness in Resource-Constrained Workflow Nets
- Introduction
- Preliminaries
- Asynchronous ?-PN
- Resource-Constrained Workflow Nets
- Undecidability of Dynamic Soundness
- Step 1: Getting Ready
- Step 2: Setting the Initial Marking
- Step 3: Simulating N
- Step 4: Reducing Reachability to Dynamic Soundness
- Undecidability
- Decidability of Dynamic Soundness for a Subclass of rcwf-nets
- Conclusions and Future Work
- References
- SimGrid MC: Verification Support for a Multi-API Simulation Platform
- Introduction
- State of the Art
- The SimGrid Framework
- SimGrid Architecture
- The Simulation Loop
- Model Checking Distributed Programs in SimGrid
- SimGrid MC
- Partial Order Reduction for Multiple Communication APIs
- Experimental Results
- SMPI Experiments
- MSG Experiment: CHORD
- Conclusions and Future Work
- References
- Ownership Types for the Join Calculus
- Introduction
- Ownership Types
- A Typed Join Calculus with Owners: J_OT
- Syntax
- Semantics
- The Type System
- Soundness of the Type System
- Secrecy in the Context of an Untyped Opponent
- An Auxiliary Type System: J_AU
- The Common Framework
- Secrecy Theorem
- Related Work
- Conclusion
- References
- Contracts for Multi-instance UML Activities
- Introduction
- Related Work
- A Load Balancing Client - Server Example
- Contracts for Multi-instance Activities
- Other Types of Multiplicity
- Concluding Remarks
- References
- Annotation Inference for Separation Logic Based Verifiers
- Introduction
- VeriFast: A Quick Tutorial
- A Singly Linked List
- Predicates
- Recursive Predicates
- Lemmas
- Automation Techniques
- Auto-Open and Auto-Close
- Autolemmas
- Automatic Shape Analysis
- Comparison
- Related Work
- Conclusion
- References
- Analyzing BGP Instances in Maude
- Introduction
- Background
- BGP
- Rewriting Logic and Maude
- A Maude Library for Encoding BGP Protocols
- Network State
- Protocol Dynamics
- Route Oscillation Detection Support
- Specifying BGP Instance
- eBGP Instance
- iBGP Instance
- Analysis
- Network Simulation
- Route Oscillation Detection
- Case Studies
- Related Work
- Conclusion and Future Work
- References
- Author Index
