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.
Domaines
Génie logiciel [cs.SE]| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...