Séminaire du 6 mars 2015




Lieu

LIP6, salle 25-26/101 comment y aller

Programme

14h00-15h00: Didier Buchs, Université de Genève, "Construire un outil de vérification symbolique depuis une description formelle d’un langage:
Diagrammes de décisions et techniques opérationnelles",

et

15h00-15h30 : Edmundo Lopez, Université de Genève, "Construire un outil de vérification symbolique depuis une description formelle d’un langage:
Traduire une description formelle en techniques opérationnelles".

Abstract (les deux exposés): transparents transparentsThe main limit towards practical model-checking is the combinatorial explosion of the number of states. Among numerous solutions proposed to tackle this problem, Decision Diagrams (DDs) have been proved efficient. They are however low-level data structures: translating a high-level model to them can be cumbersome. Indeed, little work towards their better usability has been undertaken.

We propose an abstract mechanism for the manipulation of DDs, where system transitions are described in terms of rewrite rules. We describe how basic rewrite rules can be assembled through strategies, to describe complex transition relations (e.g. involving various levels of synchronization among parallel components). The strategies and rewrite rules offer a higher-level interface, where the nature of underlying DD is hidden, close to high-level languages used to model concurrent systems. We also describe specific strategies that we use to automatically translate high-level modeling languages (namely Petri Nets and imperative languages) to rewrite strategies, ultimately translated in terms of operations on DDs.

15h30-16h00: pause café

16h00-16h30: vie du groupe