IFIP TC6 Open Digital Library

33. FORTE / 15. FMOODS 2013: Florence, Italy

Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings

Dirk Beyer, Michele Boreale

Springer, Lecture Notes in Computer Science 7892, ISBN: 978-3-642-38591-9



Contents

Invited Talk

Analyzing Interactions of Asynchronously Communicating Software Components - (Invited Paper).

Tevfik Bultan

 1-4

Session 1: Verification

Formal Analysis of a Distributed Algorithm for Tracking Progress.

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

 5-19

A Case Study in Formal Verification Using Multiple Explicit Heaps.

Wojciech Mostowski

 20-34

Parameterized Verification of Track Topology Aggregation Protocols.

Sergio Feo Arenis, Bernd Westphal

 35-49

Session 2: Types

Monitoring Networks through Multiparty Session Types.

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

 50-65

Semantic Subtyping for Objects and Classes.

Ornela Dardha, Daniele Gorla, Daniele Varacca

 66-82

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

Viviana Bono, Luca Padovani, Andrea Tosatto

 83-98

Session 3: Testing

Passive Testing with Asynchronous Communications.

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

 99-113

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

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

 114-129

Session 4: DisCoTec Joint Session

Model Checking Distributed Systems against Temporal-Epistemic Specifications.

Andreas Griesmayer, Alessio Lomuscio

 130-145

Session 5: Model Checking

Formal Verification of Distributed Branching Multiway Synchronization Protocols.

Hugues Evrard, Frédéric Lang

 146-160

An Abstract Framework for Deadlock Prevention in BIP.

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

 161-177

Bounded Model Checking of Graph Transformation Systems via SMT Solving.

Tobias Isenberg 0002, Dominik Steenken, Heike Wehrheim

 178-192

Session 6: Automata

Verification of Directed Acyclic Ad Hoc Networks.

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine

 193-208

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

Jay Thakkar, Aditya Kanade, Rajeev Alur

 209-224

Asynchronously Communicating Visibly Pushdown Systems.

Domagoj Babic, Zvonimir Rakamaric

 225-241

Session 7: Distribution and Concurrency

A Timed Component Algebra for Services.

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

 242-257

Probabilistic Analysis of the Quality Calculus.

Hanne Riis Nielson, Flemming Nielson

 258-272

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

Antonio Flores-Montoya, Elvira Albert, Samir Genaim

 273-288

Session 8: Security

Lintent: Towards Security Type-Checking of Android Applications.

Michele Bugliesi, Stefano Calzavara, Alvise Spanò

 289-304

Honesty by Typing.

Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino

 305-320