Bonjour à tous, La prochaine séance du séminaire MeFoSyLoMa sera orientée outils, et se tiendra au LRDE. ======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/ Méthodes Formelles pour Les Systèmes Logiciels et Matériels Vendredi 8 avril 2016, 14h-17h Adresse: LRDE (Epita), Salle Alpha Bâtiment X, 2e étage 18 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : https://www.google.com/maps?q=48.8152808,2.3623765 https://www.lrde.epita.fr/~adl/dl/acces-lrde.pdf 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-14h45: Alexandre Duret-Lutz (LRDE/Epita) Spot 2.0 Je présenterai Spot 2.0, une bibliothèque C++ de manipulation d'omega-automates pour le model checking. Les nouveautés sont assez nombreuses: la bibliothèque travaille maintenant avec des automates dont la condition d'acceptation peut être arbitrairement complexe (par exemple une combinaison booléenne de Streett et Rabin généralisé), de nouveaux outils en ligne de commande permettent de manipuler et produire ces automates, et la majeur partie des fonctionnalités est utilisable avec une surcouche de bindings pour Python. Je montrerai en particulier: - des exemples d'utilisation tirés du cours d'initiation au model checking de l'Epita (travail sur la sémantique de LTL, et écriture d'un model checker jouet en quelques lignes de Python). - la facilité avec laquelle on peut chaîner les différents outils pour construire un pipeline de manipulation d'automates - une technique utilisant un SAT-solver pour synthétiser des automates équivalents mais avec d'autres conditions d'acceptation. 14h45-15h30: Maximilien Colange (ENS de Cachan) Je présenterai TiAMo, un model-checker pour les systèmes temporisés développé au LSV. Les systèmes temporisés présentent une composante en temps continu, qui font de leurs espaces d'états des graphes infinis à branchement infini. Dans le cadre du model-checking, leur analyse repose essentiellement sur des abstractions permettant de se ramener à des graphes discrets. Nous nous concentrons sur les problèmes d'accessibilité dans les automates temporisés, et d'accessibilité optimale dans les automates temporisés à coûts positifs. TiAMo est pensé comme une plateforme permettant la comparaison expérimentale des différents algorithmes et abstractions pour la vérification de systèmes temporisés. Je rappellerai les principaux problèmes algorithmiques qui se posent dans ce cadre, et les différentes solutions qui ont été proposées. Je présenterai également l'outil TiAMo, et les algorithmes d'analyse qu'il implémente. 15h30-16h00: pause café 16h00: vie du groupe ======================================================================== -- Alexandre Duret-Lutz