Jessica RAVAKAMBININTSOA a soutenu sa thèse le 31/08/2026.
Lieu : amphithéâtre Clémence Royer, Bâtiment 321, Jacqueline Ferrand, Dept. GM, INSA Lyon, Villeurbanne
Chaîne automatisée de modélisation et de vérification formelle de programmes API
Jury :
Rapporteurs :
M. Bernard RIERA , Professeur des Universités, Université de Reims
M. Pascal BERRUET, Professeur des universités, Université de Bretagne Sud
Examinateurs :
Mme Pascale MARANGE, Maître de conférences, Université de Loraine
M. Alexandre PHILIPPOT, Professeur des universités, Université de Reims
Encadrement :
M. Eric ZAMAÏ , Professeur des universités, Ampère INSA-Lyon, directeur de thèse
M. Emil DUMITRESCU, Maître de conférences, Ampère INSA-Lyon, co-encadrant
Résumé :
L’automatisation industrielle repose largement sur les automates programmables industriels (API), qui assurent l’exécution des programmes de commande au cœur des procédés. Avec l’augmentation de la complexité des systèmes et de leur interconnexion, les programmes API deviennent plus étendus, plus hétérogènes et plus difficiles à analyser. Les approches classiques fondées principalement sur les tests et les relectures manuelles ne suffisent plus à garantir l’absence d’erreurs dans l’ensemble des scénarios d’exécution pertinents. Cette difficulté est renforcée par la diversité des langages définis dans la norme IEC61131-3 et par l’hétérogénéité des représentations utilisées dans les environnements industriels.
Cette thèse propose un cadre méthodologique destiné à faciliter la modélisation et la vérification formelle des programmes API. La démarche repose sur une chaîne de transformation progressive du code vers plusieurs représentations intermédiaires permettant de structurer le flot de contrôle, les dépendances de données et la dynamique cyclique du programme. Ces modèles servent de support à l’expression des propriétés à vérifier ainsi qu’à l’application de techniques formelles adaptées, notamment l’analyse statique et le model checking.
Une méthode de traduction automatique a été développée afin de générer des modèles formels exploitables à partir de programmes API réels, tout en limitant la dépendance à une expertise avancée en méthodes formelles. L’ensemble de la démarche a été intégré dans un environnement industriel existant afin de faciliter son utilisation dans un contexte de développement réel.
L’étude expérimentale menée sur des programmes représentatifs montre que les modèles générés permettent d’obtenir des analyses cohérentes et exploitables pour la vérification de propriétés locales et globales. Les résultats obtenus mettent également en évidence l’intérêt des représentations intermédiaires pour améliorer la compréhension du comportement des programmes et faciliter leur analyse.
Dans son ensemble, cette thèse contribue à rapprocher les méthodes formelles des pratiques industrielles liées aux programmes API et ouvre la voie à une utilisation plus large de ces approches dans les contextes où les exigences de sûreté et de fiabilité sont critiques.
Mots-clés :
Automates programmables industriels, automatisation industrielle, vérification formelle, méthodes formelles, model checking, analyse statique, représentations intermédiaires, IEC 61131-3, traduction automatique, sûreté, fiabilité