Conception, Formalisation et Analyse

Responsable : François Vernadat 

La maîtrise de la complexité toujours plus grande des systèmes critiques, la nécessité d'atteindre les niveaux de qualité requis, l'augmentation de la productivité, nécessitent d'améliorer les méthodes et outils d'ingénierie des systèmes. Les techniques de description formelles (TDF), par leur bases mathématiques, l'existence de techniques de vérification automatiques et d'outils supports, offrent une réponse face à cette complexité. Les TDF constituent l´objet de nos recherches qui portent sur les modèles formels, les techniques de vérification associées et les outils les supportant.
Notre objectif est d'accroitre l'expressivité de ces techniques notamment sur les aspects temporels, l'efficacité des algorithmes de vérification associés et l'intégration de ces techniques formelles dans les processus d'ingénierie systèmes.

Dans ce contexte, nos études portent sur les modèles permettant d'exprimer le parallélisme, la communication et les contraintes temporelles et plus précisément la modélisation des mécanismes de suspension/reprise souvent rencontrés dans les systèmes régis par des ordonnanceurs préemptifs. Pour analyser ces modèles, nous proposons des algorithmes de vérification (semi-algoritmes et sur-ap pro xima tion pour les modèles où l'accessibilité est indécidable) et les optimisons pour favo riser leur passage à l'échelle.

Pour valider nos modèles et les techniques de vérification associées nous les outil lons en développant la boîte à outils TINA (Time Petri Net Analyzer) qui permet l'édition, l'animation et la vérification par model-checking de réseaux de Petri temporels étendus par des données, des priorités et des chronomètres. Nous définissons le langage FIACRE (Format Intermédiaire pour les Architectures de Composants Répartis Embarqués) en collaboration avec le projet VASY /INRIA et l'équipe Acadie/IRIT et l'outillons dans le cadre du projet Topcased du Pôle de compétitivité AE/SE.

Les sujets de recherche principaux ont donc trait:
  • Au couplage des approches formelles et « métier »,
  • Aux techniques de description et de vérification des sytèmes temps réels,
  • A la représentation symbolique d'espaces d'états,
  • A la réduction de l'explosion combinatoire,
  • A la parallélisation des algortihmes de model-checking

Ces travaux sont soutenus par des projets contractuels. Pour de plus amples informations sur ces travaux de recherches, les projets ou les publications, référez-vous aux pages suivantes: