Modélisation et vérification d'un réseau de communication embarqué avec FIACRE/TINA - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Document Associé À Des Manifestations Scientifiques Année : 2013

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

Résumé

In this poster, we present our thesis work on modelisation and verification with FIACRE/ TINA. First, we build a formal model of our case study with FIACRE, a formal language to represent both the behavioural and timing aspects of real time systems. Then we exploit its structural symmetries to minimize the combinatorial explosion. TINA is a tool for the analysis of Time Petri Net. It allows for the model-checking of LTL formula on a state space abstraction of a TPN. We extend FIACRE and TINA for the specification and reduction of symmetry. First experimental results are shown.
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.
Fichier principal
Vignette du fichier
Bourdil.pdf (109.01 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00876644 , version 1 (25-10-2013)

Identifiants

  • HAL Id : hal-00876644 , version 1

Citer

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⟩
414 Consultations
330 Téléchargements

Partager

Gmail Facebook X LinkedIn More