FRIDA 2017

 

The 4th Workshop on

Formal Reasoning in Distributed Algorithms (FRIDA 2017)

October 16, 2017 (room Edison I)

Satellite workshop of DISC 2017 (Vienna, Austria)

Last minute updates:

  • The lunch schedule of FRIDA aligns with the other workshops: the lunch time is 12:30-14:00.
  • The talk by Maria Potop-Butucaru starts at 14:00.
  • The talk by Tali Sznajder starts at 14:30.
  • The talk by Sylvain Conchon starts at 15:00.
  • The talk on “Verifying Fault-tolerance in Parameterised Multi-Agent Systems” will be given by Edoardo Pirovano at 17:30.

Please do not forget to register for FRIDA’17 at the DISC’17 registration page.

Preliminary program

See the abstracts below

08:30 Alexey Gotsman
Modular verification of consensus protocols
09:00 Ahmed Bouajjani Verifying Event-Driven Asynchronous Programs against Concurrency
09:30 Christoph Sprenger The verification of a secure internet architecture
10:00 Ezio Bartocci Monitoring Mobile and Spatially Distributed Cyber-Physical Systems

 10:30 – 11:00 coffee break

11:00 Sergio Rajsbaum Tasks, objects, and the notion of a distributed problem
11:30 Pierre Fraigniaud On the various aspects of distributed decision
12:00 Gustavo Petri (U Paris 7) Strong Invariants for Weak Consistency

12:30 – 14:00 lunch break

14:00 Maria Potop-Butucaru Models for mobile robots from continus to discrete spaces
14:30 Tali Sznajder Parameterized Verification of Algorithms for Oblivious Robots on a Ring
15:00 Sylvain Conchon  Cubicle : a model checker for parameterized array-based transition systems

 15:30 – 16:00 coffee break

16:00 Cezara Dragoi Partially synchronous programming abstractions for replicated state machine
16:30 Thibaut Balabonski Certified Gathering of Oblivious Mobile Robots
17:00 Philippe Queinnec Describing asynchronous communications in distributed algorithms
17:30 Edoardo Pirovano Verifying Fault-tolerance in Parameterised Multi-Agent Systems

Summary of the workshop

Distributed algorithms is an active research field; their applications range from Internet applications over cloud computing to safety-critical control systems. Whereas many applications are of critical importance, the correctness of distributed algorithms is usually based on very subtle mathematical arguments. Consequently, one easily can make mistakes with hand-written proofs, which reduces the trust in the correctness of these systems.

In the last decades, formal methods were proven to be useful for the verification of many hardware and software systems. For distributed algorithms, the application of formal methods was limited: formal methods have been used for finding bugs in distributed algorithms, and to a much smaller extent formal methods were used in computer-aided verification of simple distributed algorithms. However, to verify more involved distributed algorithms, one cannot easily apply existing verification tools. To be eventually able to do this, an interdisciplinary effort from the concerned fields of formal methods, logic in computer science, and distributed algorithm theory is required.

The topics of interest for the third FRIDA workshop are:

  • models for distributed algorithms
  • model checking
  • proof assistants & theorem proving
  • parameterized model checking
  • integration of different verification techniques
  • concurrency
  • distributed algorithm theory
  • benchmark distributed algorithms
  • fault tolerance
  • synthesis
  • automated code generation for distributed systems
  • run-time verification of distributed systems

Confirmed Speakers

  • Sergio Rajsbaum. Tasks, objects, and the notion of a distributed problem.
  • Christoph Sprenger. The verification of a secure internet architecture.
  • Pierre Fraigniaud. On the various aspects of distributed decision.
  • Maria Potop-Butucaru. Models for mobile robots from continus to discrete spaces.
  • Ahmed Bouajjani. Verifying Event-Driven Asynchronous Programs against Concurrency.
  • Edoardo Pirovano & Alessio Lomuscio. Verifying Fault-tolerance in Parameterised Multi-Agent Systems.
  • Ezio Bartocci. Monitoring Mobile and Spatially Distributed Cyber-Physical Systems.
  • Alexey Gotsman. Modular verification of consensus protocols.
  • Gustavo PetriStrong Invariants for Weak Consistency
  • Philippe Quéinnec. Describing asynchronous communications in distributed algorithms.
  • Tali Sznajder. Parameterized Verification of Algorithms for Oblivious Robots on a Ring.
  • Cezara Drăgoi. Partially synchronous programming abstractions for replicated state machine
  • Thibaut Balabonski. Certified Gathering of Oblivious Mobile Robots.
  • Sylvain Conchon. Cubicle : a model checker for parameterized array-based transition systems


Abstracts

Ezio Bartocci (TU Wien, Austria)Monitoring Mobile and Spatially Distributed Cyber-Physical Systems.

Cyber-Physical Systems (CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, spatial along with the temporal requirements play an essential role for their correct and safe execution. However, the local interactions among the system components result in global spatio-temporal emergent behaviors often impossible to predict at the design time. In this work we pursue a complementary approach by introducing STREL a novel spatio-temporal logic that enable the specification of spatio-temporal requirements and to monitor them over executions of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic with two novel spatial operators reach and escape from which is possible to  derive other spatial modalities such as everywhere, somewhereand surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbours, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimisation. We prove that for certain models, all the spatial properties expressed with reach and escape using euclidean distance satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for  STREL and to demonstrate  the feasibility of our approach, we show its application using the monitoring of a simulated mobile ad-hoc sensor network as our running example.

Thibaut Balabonski (Université Paris Sud & LRI, France)Certified Gathering of Oblivious Mobile Robots.

Swarms of mobile robots have recently attracted the focus of the Distributed Computing community. One of the fundamental problems in this context is that of gathering the robots: the robots must meet at a common location, not known beforehand. Despite its apparent simplicity, this problem proved quite hard to characterise fully, due to many model variants, leading to informal error-prone reasoning.

Over the past few years, a significant effort has resulted in the set up of a formal framework, relying on the Coq proof assistant, that was used to provide certified results related to the gathering problem. We will see the main abstractions that permit to reason about oblivious mobile robots that evolve in a bidimensional Euclidean space, the distributed executions they can perform, and the variants of the gathering problem they can solve or they cannot solve.

Maria Potop-Butucaru (UPMC – LIP6, France)Models for mobile robots from continus to discrete spaces.

This talk will present several models for mobile robots networks starting with mobile robots in 2D and 3D continuos spaces and finishing with robots in discrete spaces. The talk would like to brig to the attention of formal methods community these models for two main reasons. First, many distributed algorithms in these models are difficult to prove  especially when the system is asynchronous. Second, many problems are open and solutions are difficult to find manually. We advocate that these models can heavily benefit from the expertise of formal methods community.

Ahmed Bouajjani (Univ. Paris Diderot (Paris 7), France)Verifying Event-Driven Asynchronous Programs against Concurrency.

We define a correctness criterion, called robustness against concurrency, for a class of event-driven asynchronous programs that are at the basis of modern UI frameworks in Android, iOS, and Javascript. A program is robust when all possible behaviors admitted by the program under arbitrary procedure and event interleavings are admitted even if asynchronous procedures (respectively, events) are assumed to execute serially, one after the other, accessing shared memory in isolation. We characterize robustness as a conjunction of two correctness criteria: event-serializability (i.e., events can be seen as atomic) and event-determinism (executions within each event are insensitive to the interleavings between concurrent tasks dynamically spawned by the event). Then, we provide efficient algorithms for checking these two criteria based on polynomial reductions to reachability problems in sequential programs. This result is surprising because it allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity. We demonstrate via case studies on Android apps that the typical mistakes programmers make are captured as robustness violations, and that violations can be detected efficiently using our approach.

This is a joint work with Michael Emmi, Constantin Enea, Burcu Kulahcioglu-Ozkan, and Serdar Tasiran.  

Sylvain Conchon (Université Paris-Sud 11, France)Cubicle : a model checker for parameterized array-based transition systems.

In this talk, I will present Cubicle, a model checker for verifying safety properties of array-based systems, a syntactically restricted class of para­metrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. After a short presentation of the semantics of its input language, I will present some details about its implementation, mainly its symbolic backward reachability analysis which makes use of Satisfiabilty Modulo Theories.  I will conclude with a presentation of current and future works.

Cezara Drăgoi (INRIA & ENS Paris, France)Partially synchronous programming abstractions for replicated state machine.

Replication is the standard way to make distributed applications fault-tolerant. Implementing state machine replication is notoriously difficult due to asynchronous communication and the occurrence of faults, such as the network dropping messages or processes crashing.

One fundamental obstacle in having correct fault-tolerant implementations is the lack of abstractions when reasoning about their behaviors. In this talk we focus on partially synchronous programming abstractions that view asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. This view simplifies the proof arguments making systems amendable to automated verification.

Technically, we take a programming language perspective and define a domain specific language which has a partially synchronous semantics and separates the implementation of network constraints from the algorithmic computation done by processes. We validate our technique by defining partially synchronous abstractions for several state machine replication algorithms, enabling automation of the verification procedure.

Pierre Fraigniaud (CNRS, France)On the various aspects of distributed decision.

This talk will survey various aspects of distributed decision, and their impacts on the theory of distributed computing, as well as their applications to distributed verification and robust computing. Distributed decision is characterized by a distributed system formed by collection of computing entities connected via some medium of communication, and a system predicate potentially expressed using specific logics. The computing entities must collectively determine whether the system is in a correct state with respect to the predicate. Distributed decision has been the subject of an abundant literature during the last decade. This talk will survey this literature, in classifying the different approaches of distributed decision, and their potential applications to related fields such as distributed system verification and fault-tolerant distributed computing.

Alexey Gotsman (IMDEA Software Institute, Spain)Modular verification of consensus protocols.

TBA

Edoardo Pirovano and Alessio Lomuscio (Imperial College London, UK)Verifying Fault-tolerance in Parameterised Multi-Agent Systems.

The talk will be given by Edoardo Pirovano.

I will present a method to evaluate the fault-tolerance of a multi-agent system whose number of agents is unknown at design time. Specifically, I will present a technique for injecting a variety of non-ideal behaviours, or faults, studied in the safety-analysis literature into the abstract agent templates that are used to generate an unbounded family of multi-agent systems with different sizes. We will define the parameterised fault-tolerance problem as the decision problem of establishing whether any concrete system, in which the ratio of faulty versus non-faulty agents is under a given threshold, satisfies a given temporal-epistemic specification. I will describe a sound and complete technique for solving the problem for the semantical set-up considered. I will also present an implementation and a case study identifying the threshold under which the alpha swarm aggregation algorithm is robust to faults against its temporal-epistemic specifications.

Joint work with Panagiotis Kouvaros

Gustavo Petri (Université Paris Diderot — Paris 7, France)Strong Invariants for Weak Consistency.

In this talk I will explore different weak consistency criteria from the standpoint of the invariants that they can guarantee without additional programmer instrumentation. I will show how some invariants are related to the guarantees provided by the different criteria, and how they help to compare and classify these criteria.

This is joint work with Marc Shapiro and Masoud Saeida-Ardekani.

Philippe Quéinnec (INPT/ENSEEIHT & IRIT, France)Describing asynchronous communications in distributed algorithms.

To formally study a distributed algorithm, a obvious requirement is to have a formal specification of this algorithm. This specification can come from an informal description of the algorithm, from an algorithmic description, from the derivation of an abstract specification (e.g. by refinement)… Anyway, at one point, the distributed nature of the algorithm appears, with nodes or sites interacting with each other. At the lowest level, when deployed on a set of computers, this communication is implemented with messages on a network. However, to reason about the algorithm, the intricate and gloomy details of the interface and behavior of this network is uninteresting. Thus researchers have invented lots of different ways to describe communication. For instance, one can use shared variables with an adequate data structure to hold the messages, e.g. a set or a queue. This yields the question of choosing the right data structure, both for the correct specification of the algorithm and for an easier reasoning. This in turn gives rise to several questions on unexpected or undesired properties of the chosen representation. Order of delivery, fairness of delivery, atomicity of communication actions, non-determinism, size boundness or failures are often embedded in this representation, and it is not always clear if they are wanted or needed.

In this talk, I will present some classic ways of representing asynchronous communication and I will discuss their pitfalls. I will also present an approach we have developed to allow for a simple parameterization of the communication properties.

Sergio Rajsbaum (Universidad Nacional Autonoma de Mexico, Mexico)Tasks, objects, and the notion of a distributed problem.

The universal computing model of Turing, which was central to the birth of modern computer science, identified also the essential notion of a problem, as an input output function to be computed by a Turing machine. In distributed computing, tasks are the equivalent of a function: each process gets only part of the input, and computes part of the output after communicating with other processes.

In distributed computing tasks have been studied from early on, in parallel, but independently of sequential objects. While tasks explicitly state what might happen when a set of processes run concurrently,  sequential objects only specify what happens when processes run sequentially. Indeed, many distributed problems considered in the literature, seem to have no natural specification neither as tasks nor as sequential objects. I will give a short overview of our  work on interval-linearizability, a notion we introduced to specify objects more general than the usual  sequential objects. I will describe the bridges we establish between these two classical paradigms, and our discussions about what is a distributed problem, and what it means  to solve it.

Joint work with Armando Castañeda and Michel Raynal

Christoph Sprenger (ETH Zürich, Switzerland)The verification of a secure internet architecture.

Routing is at the heart of the Internet and has been a continual source of security problems since its expansion in the 1980s. SCION is a new approach to the Internet, which offers dramatically better security properties than we currently have. We describe a collaborative effort, the Verified SCION Project, at ETH Zurich that aims to verify SCION, going the full distance from high-level network-wide properties down to the code running on SCION routers. We will explain the issues involved, the approach we take, the progress we have made, and perspectives for the future.

The work reported on is joint work between three groups at ETH Zurich: our Information Security Group lead by David Basin, the Network Security Group of Adrian Perrig, and the Programming Methodology Group of Peter Mueller.

Tali Sznajder (LIP6, France)Parameterized Verification of Algorithms for Oblivious Robots on a Ring.

We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus  in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a discrete space with a finite number of locations (here, a ring). A large number of algorithms have been proposed working for rings whose size is not a priori fixed and can be hence considered as a parameter. Handmade correctness proofs of these algorithms have been shown to be error-prone, and recent attention had been given to the application of formal methods to automatically prove those. Our work is the first to study the verification problem of such algorithms in the parameterized case. We show that safety and reachability problems are  undecidable for robots evolving asynchronously. On the positive side, we show that safety properties are decidable in the synchronous case, as well as in the synchronous case for a particular class of algorithms. Several properties on the protocol can be decided as well. Decision procedures rely on an encoding in Presburger arithmetics formulae that can be verified by an SMT-solver. Feasibility of our approach is demonstrated by the encoding of several case studies. Results published in FMCAD’17.


Organization

Previous editions

Starting a productive dialogue between distributed algorithms and verification communities was the goal of a successful Dagstuhl Seminar “Formal Verification of Distributed Algorithms” which was held in April 2013. During this seminar, the participants agreed that a series of workshops should be held in order to strengthen the community that does research on these issues. The 1st workshop on Formal Reasoning in Distributed Algorithms took place in Vienna as part of the Vienna Summer of Logic’14 and Federated Logic Conference’14. The 2nd FRIDA workshop took place in Grenoble as part of FORTE’15. The 3rd FRIDA workshop was organized in Marrakech as part of NETYS’16.