VERification des Systèmes Temporisés CritiqueS
- vertics -
RESPONSABLE
Responsable
Cadre scientifique
Stagiaire
Dernières Publications
2024
Communications dans un congrès
2023
Articles dans une revue
Communications dans un congrès
Autres documents
Pré-publications, documents de travail
Bernard Berthomieu, Dmitry A Zaitsev. Sleptsov Nets are Turing-complete. 2023. ⟨hal-04139308⟩
2022
Articles dans une revue
Communications dans un congrès
2021
Articles dans une revue
Communications dans un congrès
2020
Articles dans une revue
Communications dans un congrès
Pré-publications, documents de travail
2019
Articles dans une revue
Chapitres d’ouvrages
Communications dans un congrès
Autres documents
- Participation au pôle de compétitivité Aerospace Valley, pour l’écosystème Systèmes Embarqués et Communicants (SEC)
- Membre du groupe de travail IFSE (Ingéniérie Formelle des Systèmes Embarqués) au sein du RTRA STAE (Sciences et Technologies pour l'Aéronautique et l'Espace). Voir nos journées annuelles FAC (pour Formalisation des Activités Concurrentes)
- Co-organisateur du cycle de conférences FMF (Forum Méthodes Formelles)
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.
- 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.
Thèses / HDR soutenues
2023
2021
2016
2015
2014
REJOINDRE
Notre équipe de recherche
Pour plus d’informations sur les offres d’emploi, vous pouvez contacter