ACADIE Team

Head : Philippe QUEINNEC

ACADIE (Assistance à la Certification d’Applications DIstribuées et Embarquées) team is concerned with the formal and mechanized verification of systems.

Formalisation is required to assert rigorous properties on the systems, and mechanization is used to guarantee the validity of the verification.

Acadie is agnostic with regard to the used formalisms as long as they are theoretically well-founded and tool-assisted. Application domains have considered cyber-physical systems, embedded and real-time systems, distributed systems, interactive systems…

skills

formal methods
verification & validation
proof environments
cyber-physical systems
distributed systems

personnel of the team ACADIE

Permanent members
Non-permanent members
Related members

publications of the team ACADIE

Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues
Livres (monographies) Rédaction d’ouvrages de synthèse Rédaction de numéros spéciaux de revues

contrats of the team ACADIE

AcronymeTitlePeriodScientific
leaders
Partners
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
[Contract completed]
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
[Contract completed]
Vérification des optimisations rapides appliquées à la commande embarquée2013-2016Pantel, MarcCNRS (EPCST) – ONERA(EPIC) – Rockwell Collins(GE – SAS)
GeMoC
[Contract completed]
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
[Contract completed]
Méthodes catégoriques et logiques en transformations de modèles2012-2016Matthes, RalphCNRS Délégation régionale Rhône-Alpes(EPCST)
Verisync
[Contract completed]
Vérification formelle d’un générateur de code pour un langage synchrone2010-2014Strecker, MartinINRIA(EPST)
ITEmIS
[Contract completed]
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
[Contract completed]
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)
AcronymeTitlePeriodScientific
leaders
Partners
HiMoCo
[Contract completed]
Hi-Integrity Model Compiler2012-2014Pantel, MarcAdacore(PME – SAS)
OPEES
[Contract completed]
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
[Contract completed]
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
[Contract completed]
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)

[Contract completed]
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é)
Tuesday 15 October 2019, 14h00
Sur le pouvoir expressif des structures applicatives et monadiques indexées
Ian MALAKHOVSKI – Team ACADIE, IRIT UT3 Paul Sabatier, IRIT, Salle 001
#these
Friday 15 December 2017, 9h00
Formal decomposition of Event-B centralized specifications: application to BIP distributed systems
Badr SIALA – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
#these
Wednesday 22 November 2017, 10h15
Formalisation of Asynchronous Interactions
Florent CHEVROU – Team ACADIE – IRIT INP-ENSEEIHT, Salle des thèses
#these
Thursday 6 July 2017, 9h30
A formal approach for correct-by-construction system substitution
Guillaume BABIN – Team ACADIE – IRIT ENSEEIHT, Amphi A001
#these
Wednesday 5 July 2017, 9h30
Modular avionics software integration on multicore COTS: certification-compliant methodology and timing analysis metrics for legacy software reuse…
Soukayna M’SIRDI – Team ACADIE – IRIT ENSEEIHT, Amphi A001
#these
Wednesday 13 July 2016, 11h00
Systematic Use of Models of Concurrency in eXecutable Domain-Specific Modeling Languages
Florent LATOMBE – Team ACADIE – IRIT Salle du Conseil, F501
#these
Thursday 19 May 2016, 10h00
Une théorie mécanisée des arbres réguliers en théorie des types dépendants
Régis SPADOTTI – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Tuesday 29 March 2016, 14h00
Variantes de spécifications à ensembles d’acceptation pour la conception modulaire de systèmes
Guillaume VERDIER – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Salle des Thèses
#these
Friday 30 January 2015, 9h00
Formal Guaranties for Safety Critical Code Generation: the Case of Highly Variable Languages
Arnaud DIEUMEGARD – Team ACADIE – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Wednesday 10 December 2014, 10h30
Formally verified analysis of resource sharing conflicts in multithreaded Java
Nadezhda BAKLANOVA – Team ACADIE, Team MACAO – IRIT UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#these
Monday 28 October 2019 – Thursday 31 October 2019
MEDI 2019 : 9th International Conference on Model and Data Engineering
INP-ENSEEIHT
#congres Know more
Monday 26 June 2017 – Friday 30 June 2017
École Jeunes Chercheurs en Programmation 2017 (EJCP 2017)
INP-ENSEEIHT, Toulouse
#congres Know more
Monday 12 December 2016 – Friday 16 December 2016
World Champions Programming School at Toulouse
UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#congres Know more
Wednesday 18 June 2014 – Friday 20 June 2014
LACL 2014 : Logical Aspects of Computational Linguistics
UT3 Paul Sabatier, IRIT
#congres Know more
Monday 2 June 2014 – Thursday 5 June 2014
ABZ 2014 : 4th International Conference ASM, Alloy, B, TLA, VDM, Z
Toulouse
#congres Know more
Thursday 26 September 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
Wednesday 29 May 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
Friday 16 February 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
Tuesday 21 February 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
Tuesday 10 January 2017, 14h00 – 15h30
A new dimension of Cloud Governance
Ernesto PIMENTEL – Université de Malaga (Espagne) INP-ENSEEIHT, Salle des thèses
#seminaire
Monday 12 December 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
Tuesday 2 September 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
Thursday 23 January 2014, 14h00
From MTL to deterimistic timed automata
Dejan NICKOVIC – Austrian Institute of Technology (Autriche) UT3 Paul Sabatier, IRIT, Auditorium J. Herbrand
#seminaire
Friday 6 July 2018, 9h30
Formalisations pour les compositions de services
Aurélie HURAULT – Team ACADIE, IRIT INP-ENSEEIHT, Salle des thèses
#hdr
Monday 19 September 2016, 9h30
Verifying Embedded Systems
Xavier THIRIOUX – Team ACADIE – IRIT INP-ENSEEIHT, Salle des theses
#hdr
Thursday 25 June 2015
Journée du GDR GPL – Génie Logiciel et Transfert Technologique
UT3 Paul Sabatier, IRIT
#journee
Wednesday 22 April 2015 – Thursday 23 April 2015
Journées FAC’2015 : Formalisation des Activités Concurrentes
INP-ENSEEIHT, Salle des theses
#journee