Formal Techniques for Distributed Systems

1. Front Matter

   PDF

2. Invited Talk

   1. Analyzing Interactions of Asynchronously Communicating Software Components

      • Tevfik Bultan

      Pages 1-4

3. Session 1: Verification

   1. Formal Analysis of a Distributed Algorithm for Tracking Progress

      • Martín Abadi, Frank McSherry, Derek G. Murray, Thomas L. Rodeheffer

      Pages 5-19

   2. A Case Study in Formal Verification Using Multiple Explicit Heaps

      • Wojciech Mostowski

      Pages 20-34

   3. Parameterized Verification of Track Topology Aggregation Protocols

      • Sergio Feo-Arenis, Bernd Westphal

      Pages 35-49

4. Session 2: Types

   1. Monitoring Networks through Multiparty Session Types

      • Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, Nobuko Yoshida

      Pages 50-65

   2. Semantic Subtyping for Objects and Classes

      • Ornela Dardha, Daniele Gorla, Daniele Varacca

      Pages 66-82

   3. Polymorphic Types for Leak Detection in a Session-Oriented Functional Language

      • Viviana Bono, Luca Padovani, Andrea Tosatto

      Pages 83-98

5. Session 3: Testing

   1. Passive Testing with Asynchronous Communications

      • Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez

      Pages 99-113

   2. Input-Output Conformance Simulation (iocos) for Model Based Testing

      • Carlos Gregorio-Rodríguez, Luis Llana, Rafael Martínez-Torres

      Pages 114-129

6. Session 4: DisCoTec Joint Session

   1. Model Checking Distributed Systems against Temporal-Epistemic Specifications

      • Andreas Griesmayer, Alessio Lomuscio

      Pages 130-145

7. Session 5: Model Checking

   1. Formal Verification of Distributed Branching Multiway Synchronization Protocols

      • Hugues Evrard, Frédéric Lang

      Pages 146-160

   2. An Abstract Framework for Deadlock Prevention in BIP

      • Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, Fadi A. Zaraket

      Pages 161-177

   3. Bounded Model Checking of Graph Transformation Systems via SMT Solving

      • Tobias Isenberg, Dominik Steenken, Heike Wehrheim

      Pages 178-192

8. Session 6: Automata

   1. Verification of Directed Acyclic Ad Hoc Networks

      • Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine

      Pages 193-208

   2. Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels

      • Jay Thakkar, Aditya Kanade, Rajeev Alur

      Pages 209-224

   3. Asynchronously Communicating Visibly Pushdown Systems

      • Domagoj Babić, Zvonimir Rakamarić

      Pages 225-241

9. Session 7: Distribution and Concurrency

   1. A Timed Component Algebra for Services

      • Benoît Delahaye, José Luiz Fiadeiro, Axel Legay, Antónia Lopes

      Pages 242-257

   2. Probabilistic Analysis of the Quality Calculus

      • Hanne Riis Nielson, Flemming Nielson

      Pages 258-272

   3. May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects

      • Antonio E. Flores-Montoya, Elvira Albert, Samir Genaim

      Pages 273-288

This book constitutes the refereed proceedings of the 15th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2013, and the 33rd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2013, held in Florence, Italy, in June 2013, as part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013. The 20 revised full papers presented were carefully reviewed and selected from 39 submissions. The papers present a wide range of topics combining theory and practice. They cover distributed computing models and formal specification, testing, and verification methods as well as application domains such as application-level distributed systems, telecommunication services, Internet, embedded and real-time systems, and networking and communication security and reliability.

• automata
• concurrency
• model checking
• polymorphic types
• security

• Department of Computer Science and Mathematics, University of Passau, Passau, Germany

  Dirk Beyer

• Dipartimento di Sistemi e Informatica, Università di Firenze, Florence, Italy

  Michele Boreale

Policies and ethics