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)