Logiciels, Prototypes et Démonstrateurs

L’équipe Vertics développe deux outils logiciels principaux: Tina, une boîte à outils pour l'analyse de Time Petri Nets et Frac, un compilateur pour le langage de spécification Fiacre.

Tina

La Boîte à outils TINA est un ensemble d’outils pour l'édition et l'analyse des réseaux de Petri et de leurs extensions. En particulier. Tina peut gérer des réseaux de Petri temporels (TPN), des priorités, des arcs inhibiteurs, ainsi qu'une extension des TPN avec data processing appelée TTS.

Tina comprend un éditeur et une interface utilisateur graphique (nd) pour les TPN et les automates; des simulateurs et des outils de génération d'espaces d'états (tina etsift); des outils d'analyse structurelle (struct); et des model-checkers pour LTL (selt), ainsi que pour CTL* et un fragment existentiel du μ calcul (muse).

sift est une version spécialisée de tina prenant en charge la vérification à la volée des propriétés d'accessibilité. Si sift offre moins d’options que tina, il est généralement plus rapide et consomme beaucoup moins d'espace mémoire.

FIACRE

FIACRE est un langage formel intermédiaire pour la description des activités concurrentes avec contraintes temps réel. Fiacre est un langage défini formellement qui peut représenter à la fois, de manière compositionnelle, le comportement et les aspects temporels des systèmes distribués. Nous fournissons un compilateur (frac) capable de générer un modèle TTS à partir d'une spécification Fiacre donnée. Ce modèle TTS peut ensuite être utilisé avec Tina. Nous avons récemment étendu la langue avec: des fonctions du premier ordre; et des propriétés de vérification temps-réels.

Divers

Nous distribuons également plusieurs prototypes:

  • AADL2Fiacre: un plugin Eclipse, compatible OSATE, pour générer des spécifications Fiacre (comportementales) à partir d’un Modèle AADL utilisant l'Annexe Comportementale.

  • Fiacre Simulator: un plugin Eclipse fournissant un support pour l'édition, la coloration syntaxique, le débogage et la simulation des programmes Fiacre.

  • SimSo (Simulation of Multiprocessor Scheduling with Overheads): un simulateur de planification temps réel pour architectures multiprocesseurs prenant en compte, à travers des modèles statistiques, l'effet des changements de contexte et de l'accès concurrent aux caches. Le moyen le plus simple d’évaluer le simulateur est d'utiliser SimSo Web, une interface complète de SimSo sur le Web.

  • Twina: un outil d'analyse du « produit » de deux réseaux de Petri temporels (TPN). L’objectif principal de Twina est de calculer une représentation utilisable de l’intersection du language de deux TPN.

  • Ramona: un outil d'analyse en temps réel de systèmes de RAte MONotonic tAsks. Son objectif principal est de vérifier l'ordonnancabilité d'un ensemble de tâches périodiques en utilisant certaines hypothèses sur leurs exécutions; plus spécifiquement l'utilisation d'un sdcheduler à priorité fixe et d'une modèle d'exécution avec temps logique (LET).

  • MCC: un outil pour déplier des réseaux de Petri (colorés) pouvant être appliqués sur les modèles utilisés dans le Model-Checking Contest.