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 ).

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.

Recherche Laas-CNRS - Enseignement Insa de Toulouse

Quelques projets de recherche utilisant Tina

Projets en cours :

• ITEA2 OpenETCS : Open Proofs Methodology for the European Train Control Onboard System

• FNRAE - Quarteft : Langages intermédiaires et technologies de transformations qualifiables pour le développement de systèmes temps-réel.

• ARTEMIS Joint Undertaking - CESAR Cost-Efficient Methods and Processes for Safety Relevant Embedded System

Projets terminés :

• ITEA2 - Spices : Support for Predictable Integration of mission Critical Embedded Systems

• ANR Plateforme - OpenEmbeDD : Model Driven Engineering open-source platform for Real-Time Embedded systems

• FCE CRMyP - Topcased : Toolkit in OPen-source for Critical Application SystEms Development (voir également la fiche PLUME Topcased )

• ANR Arpege - ITEmIS Systèmes d'information et embarqués intégrés