Equipe ACADIE

Responsable : Philippe QUEINNEC

L’équipe ACADIE (Assistance à la Certification d’Applications DIstribuées et Embarquées) étudie le développement et la vérification de systèmes logiciels critiques pour lesquels il est nécessaire d’exhiber un certificat de correction. L’essence d’un tel certificat est une preuve mathématique de correction. L’équipe ACADIE étudie comment élaborer un tel certificat à trois niveaux :

  • Au niveau fondamental, les concepts de preuve et de calcul sont étudiés. Le cadre formel de la théorie des types et la théorie des catégories est considéré.
  • Au niveau méthode, nous étudions les concepts structurants nécessaires pour faciliter la production de preuves de correction. De plus, nous nous intéressons aux processus de production de logiciels corrects par construction. Nous considérons le développement de logiciels critiques.
  • Au niveau applicatif, nous étudions les systèmes temps réel distribués et en particulier, les systèmes embarqués critiques. Notre objectif est de comprendre les abstractions principales et les processus de développement de ce domaine applicatif, afin de fournir une assistance à la vérification de systèmes distribués critiques.

L’équipe ACADIE est structurée en trois groupes :

  • Théorie des types et théorie des catégories
  • Développement de logiciels critiques
  • Vérification de systèmes distribués critiques

Compétences

méthodes formelles
vérification & validation
environnements de preuve
systèmes cyber-physiques
systèmes répartis

personnel de l’équipe ACADIE

Membres permanents
Membres non – permanents
Membres rattachés

publications de l’équipe ACADIE

Articles dans des revues internationales
Articles dans des revues nationales
Rédaction de numéros spéciaux de revues
Conférences et workshops internationaux avec actes édités et comité de lecture
Conférences sans actes publiés
Livres (monographies) Rédaction d’ouvrages de synthèse Contributions à des ouvrages de synthèse
Thèses et habilitations
  • Kahina Hacid

    Explicitation de la sémantique du domaine dans les modèles de systèmes/ Une approche à base d’ontologies.

    Thèse de doctorat, Institut National Polytechnique de Toulouse, mars 2018.

    BibTeX

  • Aurélie Hurault

    Formalisations pour les compositions de services

    Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, juillet 2018.

    Accès : http://hurault.perso.enseeiht.fr/hdr.pdf
    BibTeX

  • Soukayna M’Sirdi

    Modular Avionics Software Integration on Multi-Core COTS : certification-Compliant Methodology and Timing Analysis Metrics for Legacy Software Reuse in Modern Aerospace Systems

    Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2017.

    Résumé
    BibTeX

  • Guillaume Babin

    A formal approach for correct-by-construction system substitution

    Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2017.

    Accès : https://www.theses.fr/2017INPT0061
    BibTeX

  • Florent Chevrou

    Formalisation of Asynchronous Interactions

    Thèse de doctorat, Institut National Polytechnique de Toulouse, novembre 2017.

    BibTeX

  • Badr Siala

    Décomposition formelle des spécifications centraliseées Event-B : application aux systèmes distribués BIP

    Thèse de doctorat, Université Paul Sabatier, décembre 2017.

    Résumé
    BibTeX

  • Xavier Thirioux

    Verifying Embedded Systems

    Habilitation à diriger des recherches, Institut National Polytechnique de Toulouse, septembre 2016.

    BibTeX

  • Florent Latombe

    Systematic use of models of concurrency in executable domain-specific modelling languages

    Thèse de doctorat, Institut National Polytechnique de Toulouse, juillet 2016.

    BibTeX

  • Guillaume Verdier

    Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes

    Thèse de doctorat, Université de Toulouse, mars 2016.

    BibTeX

  • Régis Spadotti

    Une théorie mécanisée des arbres réguliers en théorie des types dépendants

    Thèse de doctorat, Université Paul Sabatier, mai 2016.

    Résumé
    BibTeX

Rapports

contrats de l’équipe ACADIE

AcronymeTitrePériodeResponsables
scientifiques
Partenaires
DISCONTIntégration correcte de modèles discrets et continus2017-2022Singh, NeerajUniversité Paris XII Val de Marne(EPCSCP) – Telecom Paris Tech/Institut Mines Telecom(EPCST) – UL/Université de Lorraine(EPCSCP) – CLEARSY(PME)
FORMEDICISMéthodes formelles pour le développement et l’ingénierie de systèmes interactifs critiques2016-2021Ait Ameur, YamineONERA(EPIC) – ENAC/Ecole Nationale de l’Aviation Civile(Ecole) – INGENUITY i/o(SAS Société par Actions Simplifiées) – UL/Université de Lorraine(EPCSCP)
PARDIVérification de systèmes distribués paramétrés2016-2021Queinnec, PhilippeUniversité Paris VI(EPCSCP) – Université Paris XI(EPCST) – INRIA NANCY(EPCST)
IMPEX
[Contrat terminé]
Integration des semantique implicite et explicite dans le développement de systèmes discrets fondés sur la panne2013-2017Ait Ameur, YamineSupélec(EPCSCP) – Institut Telecom(EPCSCP) – SYSTEREL(PME)
VORACE
[Contrat terminé]
Vérification des optimisations rapides appliquées à la commande embarquée2013-2016Pantel, MarcCNRS (EPCST) – ONERA(EPIC) – Rockwell Collins(GE – SAS)
GeMoC
[Contrat terminé]
GeMoC : Un framework de modèles de calcul génériques pour l’éxecution et l’analyse dynamique de modèles2012-2016Cregut, XavierCNRS (EPCST) – INRIA(EPST) – OBEO(startup) – Thales(GE – SA) – ENSIETA/Ecole nationale supérieure des techniques avancées(Ecole)
CLIMT
[Contrat terminé]
Méthodes catégoriques et logiques en transformations de modèles2012-2016Matthes, RalphCNRS Délégation régionale Rhône-Alpes(EPCST)
Verisync
[Contrat terminé]
Vérification formelle d’un générateur de code pour un langage synchrone2010-2014Strecker, MartinINRIA(EPST)
ITEmIS
[Contrat terminé]
Systèmes d’information et embarqués intégrés2008-2011Filali, MamounTHC/Thales Communication (THC)(Société Anonyme) – INRIA(EPST) – ScalAgent Distributed Technologies(PME – SA) – EBM WEBSOURCING(Société Anonyme)
SPACIFY
[Contrat terminé]
Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vols spatiaux2006-2009Filali, MamounCNES(EPIC) – LABRI(Laboratoire) – Alcatel Alenia Space(Société Anonyme) – IRISA-INRIA(Laboratoire) – Télecom Bretagne/ENST Bretagne(EPCSCP)
AcronymeTitrePériodeResponsables
scientifiques
Partenaires
HiMoCo
[Contrat terminé]
Hi-Integrity Model Compiler2012-2014Pantel, MarcAdacore(PME – SAS)
OPEES
[Contrat terminé]
Plateforme ouverte pour ingénierie des systèmes embarqués2009-2012Pantel, MarcAirbus Group SAS(Grande Entreprise) – INRIA(EPST) – CS Systemes d’Informations(Etablissement de Taille Intermédiaire) – ONERA(EPIC) – Astrium(SAS Société par Actions Simplifiées) – OBEO(startup) – CEA/Commissariat à l’énergie atomique(EPIC) – Dasault Aviation(GE – SA) – Schneider Electric Industries(GE – SAS) – Thales Corporate Services(GE – SAS) – Mdba France(TPE – SARL) – Adacore(PME – SAS) – Anyware technologies(PME – SA) – Atos Origin Integration(GE – SAS) – Ingénierie Processus et Productivité(TPE – SARL)
ES-PASS
[Contrat terminé]
Embedded Systems product-based assurance2007-2009Pantel, MarcAirbus Group SAS(Grande Entreprise) – CS Systemes d’Informations(Etablissement de Taille Intermédiaire) – CEA/LIST(Laboratoire) – EADS(Société Anonyme) – ONERA(EPIC) – Thales Avionics(Grande Entreprise) – Siemens VDO automotive(Société Anonyme) – PSA PEUGEOT(GIE) – Estérel Technologies(Société Anonyme) – Astrium(SAS Société par Actions Simplifiées)
SPICES
[Contrat terminé]
Support for Predicable Integration of mission Critical Embedded Systems2006-2009Filali, MamounAirbus Group SAS(Grande Entreprise) – THC/Thales Communication (THC)(Société Anonyme) – LAAS(Laboratoire) – ONERA(EPIC) – Université de Bretagne Sud(EPCSCP)

[Contrat terminé]
GENE AUTO2006-2009Pantel, MarcBARCO(PME – SA) – Université Technique de Tallin(Institution étrangère) – Faculty of Aerospace Engineering (Institution étrangère) – Israël Aircraft Industry Ltd(Organisme étranger – Privé)
Lundi 28 Octobre 2019 – Jeudi 31 Octobre 2019
MEDI 2019 : 9th International Conference on Model and Data Engineering
INP-ENSEEIHT
#congres En savoir plus
Mardi 15 Octobre 2019, 14h00
Sur le pouvoir expressif des structures applicatives et monadiques indexées
Ian MALAKHOVSKI – Equipe ACADIE, IRIT UT3 Paul Sabatier, IRIT, Salle 001
#these
Vendredi 15 Décembre 2017, 9h00
Formal decomposition of Event-B centralized specifications: application to BIP distributed systems
Badr SIALA – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
#these
Mercredi 22 Novembre 2017, 10h15
Formalisation des interactions asynchrones
Florent CHEVROU – Equipe ACADIE – IRIT INP-ENSEEIHT, Salle des thèses
#these
Jeudi 6 Juillet 2017, 9h30
A formal approach for correct-by-construction system substitution
Guillaume BABIN – Equipe ACADIE – IRIT ENSEEIHT, Amphi A001
#these
Mercredi 5 Juillet 2017, 9h30
Modular avionics software integration on multicore COTS: certification-compliant methodology and timing analysis metrics for legacy software reuse…
Soukayna M’SIRDI – Equipe ACADIE – IRIT ENSEEIHT, Amphi A001
#these
Mercredi 13 Juillet 2016, 11h00
Systematic Use of Models of Concurrency in eXecutable Domain-Specific Modeling Languages
Florent LATOMBE – Equipe ACADIE – IRIT Salle du Conseil, F501
#these
Jeudi 19 Mai 2016, 10h00
Une théorie mécanisée des arbres réguliers en théorie des types dépendants
Régis SPADOTTI – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Mardi 29 Mars 2016, 14h00
Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes
Guillaume VERDIER – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
#these
Vendredi 30 Janvier 2015, 9h00
Garanties Formelles pour la Génération de Code Critique : l’Affaire des Langages Fortement Variables
Arnaud DIEUMEGARD – Equipe ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Mercredi 10 Décembre 2014, 10h30
Formally verified analysis of resource sharing conflicts in multithreaded Java
Nadezhda BAKLANOVA – Equipe ACADIE, Equipe MACAO – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Lundi 28 Octobre 2019 – Jeudi 31 Octobre 2019
MEDI 2019 : 9th International Conference on Model and Data Engineering
INP-ENSEEIHT
#congres En savoir plus
Lundi 26 Juin 2017 – Vendredi 30 Juin 2017
École Jeunes Chercheurs en Programmation 2017 (EJCP 2017)
INP-ENSEEIHT, Toulouse
#congres En savoir plus
Lundi 12 Décembre 2016 – Vendredi 16 Décembre 2016
World Champions Programming School at Toulouse
UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#congres En savoir plus
Mercredi 18 Juin 2014 – Vendredi 20 Juin 2014
LACL 2014 : Logical Aspects of Computational Linguistics
UT3 Paul Sabatier, IRIT
#congres En savoir plus
Lundi 2 Juin 2014 – Jeudi 5 Juin 2014
ABZ 2014 : 4th International Conference ASM, Alloy, B, TLA, VDM, Z
Toulouse
#congres En savoir plus
Jeudi 26 Septembre 2019, 14h00 – 15h00
Security and Privacy in Smart Environments
Andrey CHECHULIN – Saint-Petersbourg Institute for Informatics and Automatisation (Russie) UT3 Paul Sabatier, IRIT, Salle 003
#seminaire
Mercredi 29 Mai 2019, 14h30 – 15h30
Sécurité avec SGAC et ASTD
Marc FRAPPIER – Université de Sherbrooke, Groupe de recherche en informatique fondamentale (GRIF) (Canada) INP-ENSEEIHT, Salle des thèses
#seminaire
Vendredi 16 Février 2018, 10h30 – 12h00
Algorithmes naturels et systèmes d’influence
Bernadette CHARRON-BOST – Laboratoire d’informatique de l’École Polytechnique (LIX) (France) INP-ENSEEIHT, Salle des thèses
#seminaire
Mardi 21 Février 2017, 16h00 – 17h30
Symbolic Dynamics, Asymptotic Combinatorics and Game Theory
Nicolaï VASILYEV – Inst. de Mathématiques Steklov, St. Petersbourg (Russie) UT3 Paul Sabatier, IRIT, Salle 001
#seminaire
Mardi 10 Janvier 2017, 14h00 – 15h30
A new dimension of Cloud Governance
Ernesto PIMENTEL – Université de Malaga (Espagne) INP-ENSEEIHT, Salle des thèses
#seminaire
Lundi 12 Décembre 2016, 14h00 – 15h30
Challenges in Certification of Model-Based Design of Cyber-Physical Systems
Alain WASSYNG – Université de Mac Master, Hamilton, Ontario (Canada) ENSEEIHT, Amphitheâtre A001
#seminaire
Mardi 2 Septembre 2014, 11h00
Verified Decision Procedures for Regular Expression Equivalence
Tobias NIPKOW – Technische Universität München (Allemagne) UT3 Paul Sabatier, IRIT, Salle des Thèses
#seminaire
Jeudi 23 Janvier 2014, 14h00
From MTL to deterimistic timed automata
Dejan NICKOVIC – Austrian Institute of Technology (Autriche) UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#seminaire
Vendredi 6 Juillet 2018, 9h30
Formalisations pour les compositions de services
Aurélie HURAULT – Equipe ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
#hdr
Lundi 19 Septembre 2016, 9h30
Verifying Embedded Systems
Xavier THIRIOUX – Equipe ACADIE – IRIT INP-ENSEEIHT, Salle des theses
#hdr
Jeudi 25 Juin 2015
Journée du GDR GPL – Génie Logiciel et Transfert Technologique
UT3 Paul Sabatier, IRIT
#journee
Mercredi 22 Avril 2015 – Jeudi 23 Avril 2015
Journées FAC’2015 : Formalisation des Activités Concurrentes
INP-ENSEEIHT, Salle des theses
#journee