Description
Date depot: 1 janvier 1900
Titre: une méthode de preuve outillée afin d'automatiser les démonstrations dans la théorie des ensembles B
Directrice de thèse:
Catherine DUBOIS (CEDRIC)
Directeur de thèse:
David DELAHAYE (LIRMM)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Le développement des applications sécuritaires est réalisé chez Siemens Transportation Systems avec la méthode B. Elle garantit que le logiciel obtenu est conforme à la spécification abstraite d'un problème, par un mécanisme de raffinement.
L'outil de référence actuel de la méthode est l'Atelier B. Suite à la saisie des spécifications et des raffinements, celui-ci permet de générer les obligations de preuve qu'il faut démontrer pour valider la correction du développement. L'assistant à la preuve de l'Atelier B aide la démonstration mais il n'est pas possible de tout démontrer dans celui-ci. Il est nécessaire d'introduire des lemmes intermédiaires qui sont démontrés manuellement ou dans un outil externe.
Etant donnée la complexité des projets industriels, la preuve est une activité importante. La qualité et le coût de celle-ci doivent être maitrisés car il faut valider la correction formelle des modèles dans des délais imposés. Afin d'assurer la maîtrise de la démonstration des développements B, Siemens Transportation Systems développe des outils de preuve complémentaire à ceux déjà existants. Au fur et à mesure des développements, l'étude de nouvelles pistes a fait émerger des questions théoriques sur la coopération entre systèmes de preuve et la démonstration automatique dans la théorie des ensembles B.
Siemens Transportation Systems développe un environnement de preuve B_CARe (contrôle automatique de règles ajoutées) en complément du démonstrateur de théorème de l'Atelier B. Ces outils interviennent pour démontrer certaines propriétés lorsque celles-ci ne le sont pas au sein de l'Atelier B. Dans ce cas, une propriété au format Atelier B, aussi appelé règle, est transformée, après des contrôles, en plusieurs lemmes afin de démontrer le type, la bonne définition et le corps de la règle dans l'assistant à la preuve Coq.
L’objectif de cette thèse consiste à accroître l’automatisation au sein de l’atelier B et de ce fait réduire significativement les coûts de développement en déchargeant automatiquement un maximum d’obligations de preuve. Plus précisément, il s’agira de travailler au niveau de l’outil B_CARe, qui permet de valider (automatiquement ou non) des règles que l’on souhaite ajouter à la théorie de B.
Doctorant.e: Jacquel Melanie