Logo IRISA logo Inria

Prochains Exposés

mercredi 26 avril, 14h en salle Aurigny

Philippe Dague

Using Incremental SAT for Testing Diagnosability of Distributed DES

We extend in this work the existing approach to analyse diagnosability in discrete event systems(DES) using satisfiability algorithms (SAT), in order to analyse the diagnosability in distributed DES (DDES) and we test this extension. For this, we handle observable and non observable communication events at the same time. We also propose an adaptation to use incremental SAT over the existing and the extended approaches to overcome some of the limitations, especially concerning the length and the distance of the cycles that witness the non diagnosability of the fault, and improve the process of dealing with the reachability limit when scaling up to large systems.

jeudi 27 avril, 14h en salle Lipari

Josef Widder

Model Checking Fault-tolerant Distributed Algorithms

Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time. In the last two decades we have witnessed a revolutionary progress in software model checking due to the development of powerful techniques such as abstract model checking, SMT solving, and partial order reduction. Still, model checking of fault-tolerant distributed algorithms poses multiple research challenges, most notably parameterized verification: verifying an algorithm for all system sizes and different combinations of faults. I will present our recent results in this area which extend and combine abstraction, partial orders, and bounded model checking. Our results demonstrate that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of fault-tolerant distributed algorithms. Joint work with Igor Konnov, Marijana Lazic, and Helmut Veith

Exposés des semaines suivantes

jeudi 18 mai, 14h en salle Aurigny

Simon Lunel

To be announced

To Be announced

jeudi 8 juin, 14h en salle Aurigny

Loïc Hélouët

To be announced

To Be announced

jeudi 15 juin, 14h en salle Aurigny

Béatrice Bérard

To be announced

To Be announced

Séminaire autour des thèmes 68NQRT