Tina

Fiche logiciel validé
  • Création ou MAJ importante : 04/01/12
  • Correction mineure : 04/01/12
Mots-clés
Pour aller plus loin
  • Fiches logiciel PLUME connexes : Topcased

Tina : édition et analyse des réseaux de Petri et des réseaux temporels

Une fiche Dév Ens Sup est en relation avec cette fiche, consultez-la pour plus d'informations : Tina
Description
Fonctionnalités générales

Tina est une boîte à outils pour l'édition et l'analyse des réseaux de Petri et des réseaux temporels, développée dans le groupe OLC du LAAS/CNRS.

La boîte à outils Tina inclut les outils suivants :

  • nd (NetDraw) : Un éditeur textuel et graphique pour réseaux de Petri, réseaux de Petri temporels et automates. nd est connecté aux outils d'analyse ci-dessous.
  • tina : Construction d'espaces d'états. Les réseaux d'entrée peuvent être sous forme textuelle ou graphique. Les graphes produits peuvent l'être sous forme graphique ou textuelle. Différents formats de sortie sont disponibles pour permettre la connexion à d'autres model-checkers ou equivalence-checkers. Suivant les options, l'outil construit :

    • Le graphe de couverture d'un réseau de Petri (technique de Karp et de Miller)
    • Le graphe des marquages d'un réseau borné (le caractère borné étant vérifié à la volée)
    • Des graphes partiels utilisant différentes techniques d'exploration "ordre partiel" (graphes de pas, ensembles persistents, ...)
    • Diverses abstractions de l'espace d'états pour des réseaux de Petri temporels (graphes de classes d'états). Selon l'option choisie, les abstractions obtenues préservent les marquages, les états, les propriétés LTL, ou les propriétés de CTL*.
  • simulateur : Intégré à l'éditeur nd. Permet une simulation pas à pas de réseaux de Petri et réseaux de Petri temporels. La simulation peut être effectuée en mode textuel ou graphique. Différentes facilités sont offertes pour la gestion des scénarios.

  • struct : Analyse structurelle des réseaux de Petri. Calcul des ensembles de flôts et de semi-flôts du réseau sur les places ou les transitions. Détermine les propriétés de consistance et d'invariance.
  • plan : Analyse de chemin dans les réseaux de Petri temporels. Calcule un ou tous les échéanciers temporels associés à une séquence de transitions. Possibilité d'obtenir le chemin le plus lent et le plus rapide.
  • selt : Model-checker pour la logique State/Event-LTL. Il peut être utilisé en ligne de commande ou en mode interactif. Permet de définir de nouveaux opérateurs et de redéfinir les opérateurs existants. En cas de formule non satisfaite, le contre-exemple obtenu peut être rejoué interactivement dans le simulateur.
    La conversion de la formule en automate de Buchi est assurée par l'outil externe ltl2ba
  • ndrio : Outil de conversion entre différents formats de réseau de Petri: .net, .ndr and .tpn (formats natifs de Tina), et .pnml ( Petri Net Markup Language ).
  • ktzio : Outil de conversion entre différents formats de systèmes de transitions de Kripke: .ktz (format compressé natif de Tina), .aut et .bcg (formats CADP ).
Interopérabilité

Les espaces d'états produits par TINA peuvent être produit aux formats .aut ou .bcg pour la boîte à outils CADP.
D'autre part, un certain nombre d'outils importent et/ou exportent des réseaux au formats de Tina, notamment :
- exp.open de la boîte à outils CADP exporte des réseaux d'automates décrits dans le langage d'EXP 2.0 (fichier .exp) dans le format .tpn de Tina.
- Deborah décompose des réseaux de Petri décrits aux formats de Tina dans des sous-réseaux fonctionnels, permettant un calcul plus rapide des invariants.
- Helena , un model-checker pour les réseau de Petri colorés, peut déplier des réseaux colorés dans le format .net de Tina.
- PEP , une boîte à outils pour réseaux de Petri, peut invoquer les facilités de construction d'espaces d'états de Tina pour les réseaux temporels. Elle contient aussi un convertisseur de réseaux entre différents formats incluant le format de Tina.
- Romeo , un outil d'analyse pour les réseaux de Petri temporels. Il importe et exporte des réseaux au format de Tina.
- SNOOPY est un éditeur de réseaux de Petri exportant des réseaux au format Tina.

Contexte d'utilisation dans mon laboratoire/service

Recherche Laas-CNRS - Enseignement Insa de Toulouse

Quelques projets de recherche utilisant Tina

Projets en cours :

Projets terminés :

Environnement du logiciel
Plates-formes

Tina est disponible pour :

 PC sous Linux, 32 bits et 64 bits
 PC sous Windows 98/NT/XP/Vista/Seven
 PC sous SunOS 5.X (Solaris 10, OpenSolaris) 
 PPC MacIntoshes sous MacOS X 
 Intel MacIntoshes sous MacOS X 
 Sun Sparcstations sous SunOS 5.X (Solaris 8, 9, 10)
Logiciels connexes

CADP ("Construction and Analysis of Distributed Processes") est une boîte à outils développée par l'équipe VASY de l'INRIA .
La boîte à outils comprend des compilateurs pour différents formalismes d'entrée (Lotos, réseaux d'automates communicants, ...), différents outils de model-checking pour la logique temporelle ou le mu-calcul, des outils de contrôle d'équivalences de comportement (minimisation, comparaison), ...

Environnement de développement
Type de structure associée au développement
Environnement utilisateur
Liste de diffusion ou de discussion, support et forums