دانلود کتاب 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, Iceland, June 6-9, 2011 Proceedings

فهرست مطالب :

Cover
Lecture Notes in Computer Science 6722
Formal Techniques
for Distributed Systems
ISBN 9783642214608
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
Advanced Variability Management
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
back-matter