background
title
20 Septembre 2013 — Faculté des Sciences de Rabat, Université Mohammed V Agdal
estompage

Organisation

Dans le cadre d'une collaboration entre les universités Pierre & marie Curie et Mohammed V Agdal sur la conception et l'analyse de réseaux de capteurs, nous organisons une journée de travail sur le thème: «vérification formelle & réseaux de capteurs».

Cette journée se déroulera dans la salle de soutenance du bâtiment, Bâtiment du CEDoc, à la faculté des sciences de Rabat, de 09h45 à 17h30.

Le poster d'annonce est disponible ici.

L'inscription à la Journée Franco Marocaine Vérification Formelle & Réseaux de Capteurs est gratuite dans la mesure des places disponibles mais, pour des raisons d'organisation, obligatoire en envoyant la fiche d'inscription complétée à Salma Mouline avant le mardi 17 septembre 2013.

Programme

10h00-11h00: Laure Petrucci (Université Paris XIII, France), «Analyse précise de la robustesse des réseaux de Petri temporels avec arcs inhibiteurs»
Quantifier la robustesse d'un système temps-réel consiste à mesurer l'étendue maximale des délais temporels pour laquelle le système satisfait toujours sa spécificatio. Dans ce travail, nous introduisons une notion de robustesse plus précise, en mesurant les variations de délais admises dans leur voisinage. Nous considérons ici le formalisme des réseaux de Petri temporels avec arcs inhibiteurs. Nous utilisons la méthode inverse, définie initialement pour les automates temporisés. Ses résultats se présentent sous la forme de contraintes linéaires paramétrées reliant tous les délais. Nous exhibons aussi une condition et une construction pour obtenir un système robuste à partir d'un système non robuste.

11h00-11h30: pause café

11h30-12h30: Youssef Fakhri (Université Ibn Tofail, Maroc), «Réseaux Ad-hoc et réseaux de capteurs sans fil : Évaluation et optimisation de la QoS»
L’évolution et le déploiement réussi des réseaux ad hoc sans fil et les réseaux de capteurs sans fil (RCSF) dans le monde ont ouvert la voie pour un accroissement des activités de recherche, développement et standardisation dans ce domaine. Les mécanismes mis en œuvre deviennent de plus en plus complexes, ceci pour assurer des fonctions exigées par certaines applications: qualité de service, sécurité, mobilité…. Dans ce séminaire nous allons explorer le problème de l’intégration de mécanismes de qualité de service compatible avec la mobilité dans les réseaux Ad hoc sans-fil d’une part et les réseaux de capteurs sans fil d’autre part.

12h30-14h00: déjeuner

14h00-15h00: Fabrice Kordon (Université Pierre & Marie Curie, France), «Modèles hiérarchiques pour la vérification efficace de systèmes temps-réel»
Le mode checking est désormais une technique de vérification reconnue pour évaluer formellement des spécifications. Cependant, l'explosion combinatoire intrinsèque à cette technique empêche la vérification de systèmes complexes. Les cas de réseaux de capteurs, qui allient des aspects répartis avec des aspects temporisés, sont tout particulièrement concernés par ce problème.
Nous présenterons au cours de cet exposé quelques combinaisons de techniques permettant de palier ce problème. Ces combinaisons ont permis l'élaboration d'outils efficaces permettant de vérifier des systèmes plus complexes.

15h00-15h30: pause café

15h30-16h30: Yann Thiery-Mieg (Université Pierre & Marie Curie, France), «Un Langage d'Actions Guardées (GAL) pour exprimer la sémantique des systèmes»
Les structures de données symboliques comme les diagrammes de décision (BDD) sont très efficace pour le model-checking. Cependant, l'expression symbolique du système est habituellement complexe et demande une grande expertise. Nous présentons ici le langage d'actions guardées GAL, qui s'insère dans un cadre permettant la composition de spécification comportementales appelé systèmes de transitions instantiables (ITS) pour permettre de décrire de façon flexible et puissante la sémantique de systèmes concurrents manipulant des données complexe à l'aide d'une syntaxe proche du C. L'ensemble est supporté par un model-checker (CTL/LTL) très compétitif qui repose sur des diagrammes de décision.

16h30-17h30: Table ronde avec les orateurs animée par Moulay Driss Rahmani (Univ. Mohammed V Agdal, Maroc)