Séminaire du 25 septembre 2015

Lieu

ENS de Cachan, Salle Condorcet dans le Bâtiment d'Alembert: comment y aller

Programme

14h00-15h00: Thomas Chatain, ENS de Cachan, "Preserving Partial Order Runs in Parametric Time Petri Nets"

Abstract: Parameter synthesis for timed systems aims at deriving parameter valuations satisfying a given property. In this paper we target concurrent systems; it is well known that concurrency is a source of state-space explosion, and partial order techniques were defined to cope with this problem. Here we use partial order semantics for parametric time Petri nets as a way to significantly enhance the result of an existing synthesis algorithm. Given a reference parameter valuation, our approach synthesizes other valuations preserving, up to interleaving, the behavior of the reference parameter valuation. We show the applicability of our approach using acyclic asynchronous circuits.

15h00-15h30 : Mohamed Mahdi Benmoussa, UNiversité Paris 13, "Modélisation de systèmes temps-réel à l'aide de diagrammes UML et de réseaux de Petri colorés"

Abstract: Afin d'assurer la sécurité et la validation des systèmes, la vérification formelle est nécessaire. Une solution est de modéliser les systèmes en utilisant un langage de modélisation et ensuite de faire la traduction vers un modèle formel. UML est l'un des langages les plus utilisés parmi les langages de modélisation pour sa syntaxe riche et la diversité de ses diagrammes, dont les diagrammes états-transitions. Cependant, il n'y a pas de sémantique officielle décrite formellement pour UML, ce qui empêche la vérification des systèmes. Nous présenterons une méthode de spécification pour guider les concepteurs dans la modélisation des systèmes en utilisant les diagrammes états-transitions. Afin de vérifier les systèmes, nous traduisons les diagrammes états-transitions vers les réseaux de Petri colorés. La dernière partie de notre travail sera d'automatiser la traduction des diagrammes états-transitions vers les réseaux de Petri en proposant un support automatisé. En perspective nous souhaiterons valider notre traduction en prouvant l'équivalence entre le diagramme états-transitions source (en utilisant une sémantique opérationnelle) et le réseau de Petri coloré résultat.

15h30-16h00: pause café

16h00-16h30: vie du groupe