November 2014 - Annonce

exposé de Maximilien Collenge sur des automates de Büchi avec compteurs le 4 décembre au LRDE
by Alexandre Duret-Lutz 28 Nov '14

28 Nov '14

Le 4 décembre, à 14h, au LRDE (https://www.lrde.epita.fr/wiki/Contact) Maximilien Collenge, actuellement en post-doc à l'université de Genève, fera un exposé sur les automates de Büchi avec compteurs. Abstract: Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties. When the quantitative domain is discrete, quantities can be encoded as automata states, and quantitative model-checking is thus reduced to qualitative model-checking. To this end, the initial model is enhanced with new state variables that keep track of the observed quantities, while the quantitative property is rephrased as a qualitative one over the enhanced model. However, such a quantitative-to-qualitative approach lacks generality and is prone to errors, as it makes no clear distinction between the system to be verified (the actual behavior) and the property to be checked (the desired behavior). We propose a cleaner method for discrete quantitative model-checking by extending linear temporal logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This extension can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. -- Alexandre Duret-Lutz

1 0

Soutenance de thèse de E. Renault
by Etienne Renault 20 Nov '14

20 Nov '14

Bonjour, J'ai le plaisir de vous convier à ma soutenance de thèse qui aura lieu le Vendredi 5 Décembre 2014 à 14h en salle salle 211 - tour 55 - couloir 55/65 - 2ème étage. La soutenance sera suivie d’un pot. Sujet de la thèse : « Contribution aux tests de vacuité pour le model checking explicite » Membre du jury : Laure. Petrucci (Professeur à l’Université Paris 13): rapporteur Francois Vernadat (Professeur à l’INSA toulouse): rapporteur Jean-Michel. Couvreur (Professeur à l’Université d’Orléans) : examinateur Emmanuelle Encrenaz (Maitre de conférence à l’Université Paris 6): examinateur Jaco van de Pol (Professeur à l’Université de Twente): examinateur Alexandre Duret-Lutz (Maitre de conférence à l’EPITA): encadrant de thèse D. Poitrenaud (Maitre de conférence à l’Université Paris 6): encadrant de thèse Fabrice Kordon (Professeur à l’Université Paris 6): Directeur de thèse Plan d’accès : http://www.upmc.fr/fr/universite/campus_et_sites/a_paris_et_en_idf/jussieu.… Résumé : ———— L'approche automate pour le model checking de propriétés temporelles à temps linéaire est une technique classique de vérification formelle de systèmes concurrents. Un système, ainsi qu'une propriété qu'on souhaite y vérifier, sont modélisés sous forme d’omega-automates reconnaissant des mots infinis. Des manipulations de ces automates (produit synchronisé et test de vacuité) permettent d'établir si le système vérifie la propriété ou non. Dans cette thèse nous nous focalisons sur un type particulier d'omega-automates qui permettent une représentation concise des propriétés d'équité faible: les automates de Büchi généralisés basés sur les transitions (TGBA ou Transition-based Generalized Büchi Automata). Dans un premier temps, nous brossons un aperçu des algorithmes de vérification existant et nous en proposons de nouveaux traitant efficacement les automates généralisés forts. Dans un second temps, l'analyse des composantes fortement connexes de l'automate de la propriété nous a conduit à élaborer une décomposition de cet automate. Cette décomposition se focalise sur les automates multi-forces et permet une parallélisation naturelle des model-checkers. Enfin, nous avons proposé les premiers tests de vacuité parallèles pour les automates généralisés. De plus, tous ces tests sont lock-free à la différence de ceux de l’état de l’art. Toutes ces techniques ont ensuite été implémentées et évaluées sur un jeu de test conséquent. Abstract : ———— The automata-theoretic approach to linear time model-checking is a standard technique for formal verification of concurrent systems. The system and the property to check are modeled with omega-automata that recognizes infinite words. Operations overs these automata (synchronized product and emptiness checks) allows to determine whether the system satisfies the property or not. In this thesis we focus on a particular type of omega-automata that enable a concise representation of weak fairness properties: transitions-based generalized Büchi automata (TGBA). First we outline existing verification algorithms, and we propose new efficient algorithms for strong automata. In a second step, the analysis of the strongly connected components of the property automaton led us to develop a decomposition of this automata. This decomposition focuses on multi-strength property automata and allows a natural parallelization for already existing model-checkers. Finally, we proposed, for the first time, new parallel emptiness checks for generalized Büchi automata. Moreover, all these emptiness checks are lock-free, unlike those of the state-of-the-art. All these techniques have been implemented and then evaluated on a large benchmark.

1 0

[Seminaire-LRDE] Demain, Mercredi 19 novembre 2014 : Markus Voelter, independent/itemis
by Daniela Becker 18 Nov '14

18 Nov '14

Bonjour, petit rappel : la prochaine séance du Séminaire du LRDE aura lieu demain, Mercredi 19 novembre 2014 (11h30--13h), en Amphi 1. Au programme : * 11h30: Generic Tools, Specific Languages -- Markus Voelter, independent/itemis http://www.voelter.de Generic Tools, Specific Languages is an approach for developing tools and applications in a way that supports easier and more meaningful adaptation to specific domains. To achieve this goal, GTSL generalizes programming language IDEs to domains traditionally not addressed by languages and IDEs. At its core, GTSL represents applications as documents / programs / models expressed with suitable languages. Application functionality is provided through an IDE that is aware of the languages and their semantics. The IDE provides editing support, and also directly integrates domain-specific analyses and execution services. Applications and their languages can be adapted to increasingly specific domains using language engineering; this includes developing incremental extensions to existing languages or creating additional, tightly integrated languages. Language workbenches act as the foundation on which such applications are built. -- Dr. Markus Voelter works as an independent researcher, consultant and coach for itemis AG in Stuttgart, Germany. His focus is on software architecture, model-driven software development and domain specific languages as well as on product line engineering. Markus also regularly writes (articles, patterns, books) and speaks (trainings, conferences) on those subjects. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0