========================================================================

Séminaire MeFoSyLoMa http://www.mefosyloma.fr/

Méthodes Formelles pour les Systèmes Logiciels et Matériels

vendredi 18 mai 2018, 14h-16h30

Adresse: Amphi IP 11 24 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie

Plans d'accès : https://www.google.com/maps?q=48.815378,2.363106 https://www.lrde.epita.fr/~adl/img/plan-ip11.png

S'il y en a parmi vous qui comptent venir en voiture, le parking du centre commercial Okabé est gratuit pendant 3h. http://www.okabe.com/okabe/fr/okabe-parking

========================================================================

Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC), LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la confrontation de différentes approches ou points de vue sur l'utilisation des méthodes formelles dans les domaines du génie logiciel, de la conception de circuit, des systèmes répartis, des systèmes temps-réel ou encore des systèmes d'information. Il s'organise autour de réunions bimestrielles où sont exposés des travaux de recherche récents sur ce thème.

========================================================================

Programme

14h00-15h00: Étienne Renault (LRDE/EPITA), "The quest for an efficient LTL model-checking"

Abstract: Model checking is an automated verification technique that is used for establishing that a model of a system is correct with respect to some given specification. One of the most serious problems with model checking in practice is the so-called "state explosion problem", i.e the state-space of a system can be too large to be processed in a reasonable time and to be stored on the memory. This problem can be addressed using symbolic or explicit techniques. In this talk I will focus on the latter one by overviewing the recent advances in (1) emptiness checks and (2) partial-order reductions.

15h00-15h30: Mathias Ramparison (LIPN, Université Paris 13), "Timed automata with parametric updates"

Abstract: Timed automata (TAs) represent a powerful formalism to model and verify systems where concurrency is intricated with hard timing constraints. However, they can seem limited when dealing with uncertain or unknown timing constants. Several parametric extensions were proposed in the literature, and the vast majority of them leads to the undecidability of the EF-emptiness problem: "is the set of valuations reaching a given location empty?" Here, we study an extension of TAs where clocks can be updated to a parameter. While the EF-emptiness problem is undecidable for rational-valued parameters, it becomes PSPACE-complete for integer-valued parameters. In addition, exact synthesis of the parameter valuations set can be achieved. We also extend these two results to the EF-universality ("are all valuations reaching a given location?"), AF-emptiness ("is the set of valuations such that a given location is unavoidable empty?") and AF-universality ("are all valuations such that a given location is unavoidable?") problems. 15h30-16h00: pause café 16h00-16h30: vie du groupe

15h30-16h00: pause café

16h00-16h30: vie du groupe

========================================================================