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.