Modélisation et vérification d'un réseau de communication embarqué avec FIACRE/TINA

Résumé : Ce poster présente nos travaux de thèse sur l'utilisation des techniques de modélisation et de vérification avec FIACRE/TINA. Après avoir modélisé l'objet notre cas d'étude avec FIACRE, un langage formel pour la description des systèmes temps réel, nous en exploitons les symétries structurelles pour améliorer le passage à l'échelle des techniques de model-checking. TINA est un outil d'analyse des réseaux de Petri temporels. Il permet la vérification de propriétés LTL par model-checking sur une abstraction de l'espace d'états d'un TPN. Nous étendons FIACRE et TINA pour la définition et l'exploitation des symétries. Les premiers résultats expérimentaux sont présentés.
Type de document :
Document associé à des manifestations scientifiques
MSR 2013 - Modélisation des Systèmes Réactifs, 2013, Rennes, France
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00876644
Contributeur : Hervé Marchand <>
Soumis le : vendredi 25 octobre 2013 - 11:40:53
Dernière modification le : mercredi 6 juin 2018 - 16:40:02
Document(s) archivé(s) le : vendredi 7 avril 2017 - 17:39:05

Fichier

Bourdil.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00876644, version 1

Citation

Pierre-Alain Bourdil, Bernard Berthomieu, Eric Jenn, François Vernadat. Modélisation et vérification d'un réseau de communication embarqué avec FIACRE/TINA. MSR 2013 - Modélisation des Systèmes Réactifs, 2013, Rennes, France. 〈hal-00876644〉

Partager

Métriques

Consultations de la notice

392

Téléchargements de fichiers

369