AFSEC

Approches Formelles des Systèmes Embarqués Communicants

Archive pour September, 2010

Journée Outils pour les modèles temporisés et hybrides (18 novembre 2010)

Thursday 16 September 2010

Journée Afsec Outils pour les modèles temporisés et hybrides .
Le 18 novembre 2010 à l’Institut Supérieur de Mécanique de Paris - SUPMECA (Metro 13, station “Carrefour Pleyel” ou RER B, station “La Plaine–Stade de France”)
en conjonction avec les journées du GDR MACS du 18 et 19 novembre 2010.

La journée aura lieu dans l’amphi 201B (2ième étage du bâtiment historique) et sera fléchée à partir de l’accueil de l’établissement.

Programme du 18 novembre :
Accueil à partir de 8h30
Pauses café : 11h-11h30 et 16h-16h30
Repas : 13h-14h30

Programme scientifique :
Matin (9h30-13h) :

  • Alexandre David - université d’Aalborg (Danemark)
    • Peeling the layers of UPPAAL From a user’s perspective to the engine
    • abstract: In this talk we present model-checker UPPAAL from its input language and its semantics to which algorithms are used to do model-checking and how they are implemented. We show a few modeling patterns and examples to show how the tool can be used.

    • Controller synthesis with UPPAAL-TIGA
    • abstract: In this talk we present the time game extension of UPPAAL, including the algorithm, how it is implemented, and some examples.

  • Louis-Marie Traonouez “anciennement” IRCCyN
    • Vérification et dépliage des réseaux de Petri temporels, à stopwatch et paramétrés avec Roméo
    • Résumé: Romeo est un atelier logiciel pour l’édition et la vérification de réseaux de Petri temporels, et de leur extensions avec chronomètres ou paramètres temporels. Le logiciel permet une analyse à la volée de formules TCTL. Dans les dernières versions, la technique a été étendue afin de manipuler symboliquement des paramètres temporels. Nous présenterons l’intérêt d’une approche de vérification paramétrée par une démonstration de Romeo. Par ailleurs, un outil de dépliage symbolique de réseaux de Petri temporels paramétrés a été ajouté. Nous présenterons son utilisation dans une méthode de vérification par supervision de modèles.

Après midi (14h30-17h45):

  • Goran Freshe - Universite Joseph Fourier Grenoble 1 - Verimag
    • Vérification des Systèmes Hybrides avec SpaceEx
    • Nous présentons SpaceEx, un nouvel outil de vérification pour des systèmes avec dynamiques continues et discrets. Il utilise des algorithmes qui sont basés sur la représentation des ensembles continus par leur fonction de support. Cette représentation permet des manipulations approximatives d’ensembles à un coût réduit. La performance est démontrée par des exemples.

  • Bernard Berthomieu - LAAS (Toulouse)
    • Perspectives pour TINA (TIme petri Net Analyzer).
    • Résumé: TINA est une boite à outils pour l’édition, l’analyse et la vérification de systèmes temporisés décrits par des réseaux de Petri temporels étendus (par des conditions booléennes, priorités, chronomètres, traitement de données synchronisé). La vérification se fait à la volée pour des propriétés d’accessibilité, ou hors ligne par vérification de modèle pour des propriétés plus riches (LTL, Mu-Calcul) après calcul d’une abstraction adéquate de l’espace d’états.
      Nous présenterons les évolutions récentes de la boite à outils, notamment le langage de description de haut niveau Fiacre et les chaines de compilation de AADL vers Fiacre et de Fiacre vers TINA. Nous discuterons aussi de la prochaine génération des outils d’analyse, combinant compression des états et exploration parallèle pour un gain important en capacités d’analyse et de vérification.

    Publié dans Actions Afsec, Journées | Pas de commentaire »

    ISoLA 2010 et WCTT Track

    Friday 10 September 2010

    La conférence ISoLA 2010 (4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 18-20 October 2010) a un track WCTT (Worst Case Traversal Time). La communauté AFSEC/WEED y est particulièrement bien représentée avec 5 papiers sur 9.

    Publié dans Actions Afsec, Manifestations, Conférences, Conférences, WEED | Pas de commentaire »