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