ENS de Cachan, Salle Condorcet dans le Bâtiment d'Alembert: comment y aller
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.
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.