Formal Techniques for Distributed Systems

Name: Formal Techniques for Distributed Systems | Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012, Proceedings

Holger Giese Grigore Rosu(Herausgeber*in)

Springer (Verlag)

Erschienen am 9. Juni 2012

XIII, 269 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-30793-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Foreword
Preface
Organization
Table of Contents
A Reversible Abstract Machine and Its Space Overhead
Introduction
The Oz Language
A Reversible Abstract Machine for Oz
Properties of the Reversible Abstract Machine
Memory Overhead
Overhead of the Reversible Abstract Machine
Lower Bound on the Cost of Reversing Oz Programs
Discussion
Related Work
Conclusion
References
A Small Model Theorem for Rectangular Hybrid Automata Networks
Introduction
Modeling Framework
LH-Assertions
Networks of Rectangular Hybrid Automata
Example: Simple Air Traffic Landing Protocol
Semantics of RHA Networks
Small Model Theorem
Applying the Small Model Result to Check Inductive Invariants
Passel: Tool Implementation and Results
Conclusion and Future Work
References
Analysis of May-Happen-in-Parallel in Concurrent Objects
Introduction
Concurrent Objects
Operational Semantics
Definition of MHP
MHP Analysis
Inference of Method-Level MHP
The Notion of MHP Graph
Inference of Global MHP
Soundness and Complexity
Experimental Evaluation
Conclusions, Related and Future Work
References
Behavioural Equivalences over Migrating Processes with Timers
Introduction
TiMo
Syntax
Semantics
An Example
Timed Bisimulations in TiMo
Bounded Timed Bisimulations in TiMo
Relaxing Timed Bisimulations
Conclusion
References
Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs
Introduction
Preliminaries
Running Example
Symbolic Observation Graphs
Composition of SOGs
Observed Behavior
Synchronous Composition
The Observed Behavior Computation Algorithm
Related Work
Conclusion
References
Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata
Introduction
Timed Automata
Model Checking Problems
The Region Abstraction
Bounded Model Checking for Reachability and Lassos
Region-Based BMC
Ensuring Non-zenoness
Completeness
Alternative Encodings
Experiments
Conclusions
References
Conformance Testing of Boolean Programs with Multiple Faults
Introduction
Modular Visibly Pushdown Automata (MVPA)
Conformance Testing
(R, )-Conformance Testing
Lower Bounds for Conformance Testing
Specification MVPA
Lower Bound for the (R, )-Conformance Test
Conclusions
References
Knowledge-Based Distributed Conflict Resolution for Multiparty Interactions and Priorities
Introduction
The BIP Framework
Knowledge-Based Detection of False Conflicts
Knowledge and Indistinguishability
Conflict-Free Semantics
Observational Conflict-Free Semantics
Heuristics for Minimizing Observation
Implementation and Experiments
Dining Philosophers
Jukebox
Related Work
Conclusion
References
Modelling Probabilistic Wireless Networks
Introduction
Background
Networks and Their Computations
Testing Networks
Proof Techniques for the Testing Preorders
An Application: Probabilistic Routing
Conclusions
References
Noninterference via Symbolic Execution
Introduction
Background
Noninterference
Declassification
Symbolic Execution
Approach
Overview
Transformation of a Basic Language
Procedures
Dynamically Allocated Data Structures and Noninterference
Tool and Experimental Results
Tool Introduction
Implicit Flow, Explicit Flow or No Flow
While-Loop Insecure Program DarvasRep
e-Banking Example
Average Example
Password Examples
Statistics
Related Work
Conclusion
References
Defining Distances for All Process Semantics
Introduction and Motivation
Preliminaries
Simulation Distance
Bisimulation Distance
Distances for All the Semantics in the ltbt-Spectrum
Generalizations, Applications and Some Conclusions
Conclusion
References
Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata
Introduction
Timed Automata
Model Checking Problems
The Region Abstraction
Bounded Model Checking for Reachability and Lassos
Region-BasedBMC
Ensuring Non-zenoness
Completeness
Alternative Encodings
Experiments
Conclusions
References
Conformance Testing of Boolean Programs with Multiple Faults
Introduction
Modular Visibly Pushdown Automata (MVPA)
ConformanceTesting
(R,?)-Conformance Testing
Lower Bounds for Conformance Testing
Specification MVPA
Lower Bound for the (R,?)-Conformance Test
Conclusions
References
Knowledge-Based Distributed Conflict Resolution for Multiparty Interactions and Priorities
Introduction
The BIP Framework
Knowledge-Based Detection of False Conflicts
Knowledge and Indistinguishability
Conflict-Free Semantics
Observational Conflict-Free Semantics
Heuristics for Minimizing Observation
Implementation and Experiments
Dining Philosophers
Jukebox
Related Work
Conclusion
References
Modelling Probabilistic Wireless Networks
Introduction
Background
Networks and Their Computations
TestingNetworks
Proof Techniques for the Testing Preorders
An Application: Probabilistic Routing
Conclusions
References
Noninterference via Symbolic Execution
Introduction
Background
Noninterference
Declassification
Symbolic Execution
Approach
Overview
Transformation of a Basic Language
Procedures
Dynamically Allocated Data Structures and Noninterference
ToolandExperimentalResults
Tool Introduction
Implicit Flow, Explicit Flow or No Flow
While-Loop Insecure Program [8]
e-Banking Example
Average Example
Password Examples
Statistics
Related Work
Conclusion
References
Defining Distances for All Process Semantics
Introduction and Motivation
Preliminaries
Simulation Distance
Bisimulation Distance
Distances for All the Semantics in the ltbt-Spectrum
Generalizations, Applications and Some Conclusions
References
Secure Multi-Execution through Static Program Transformation
Introduction
Setting
Secure Multi-Execution: The Operational Approach
Secure Multi-Execution by Program Transformation
Implementation
Transformation to a Concurrent Language
Related Work
Conclusion
References
Synchronous Interface Theories and Time Triggered Scheduling
Introduction
Synchronous Interfaces
Semantics
Operations
Incremental TTEthernet Scheduling with SI
Conclusion and Further Work
References
TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs
Introduction
Illustrative Example
ActorSemantics
Definitions for Partial-Order Reduction
TransDPOR: A New DPOR Algorithm
Implementation and Evaluation
Related Work
Conclusions and Future Work
References
Verification of Ad Hoc Networks with Node and Communication Failures
Introduction
Ad Hoc Networks
Safety Analysis: The Control State Reachability Problem
Node Failures
Intermittent Nodes
Node Crash and Restart
Communication Failures
Message Loss
Conflict
Conflict Detection
Conclusion
References
Verification of Timed Erlang Programs Using McErlang
Introduction
Erlang
Handling Time in Erlang
McErlang
ATimedExtension
An Untimed Semantics
Adding Explicit Time
Supporting Timestamps
A Semi-formal Timed Semantics
Finite Models
Experiments
Efficiency
Expressive Power
Conclusions
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken