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
Published on 9. June 2012
XIII, 269 pages
978-3-642-30793-5 (ISBN)
Description
This book constitutes the refereed proceedings of the 14th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2012, and the 32nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2012, held in Stockholm, Sweden, in June 2012, as one of the DisCoTec 2012 events. The 16 revised full papers presented were carefully reviewed and selected from 42 submissions. They cover a wide range of topics combining theory and practice in application areas of telecommunication services, Internet, embedded and real-time systems, networking and communication security and reliability, sensor networks, service-oriented architecture, and Web services.
More details
Other editions
Additional editions
Holger Giese | Grigore Rosu
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
Book
05/2012
Springer
€53.49
Shipment within 7-9 days
Content
- 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
