Thesis of Marc Sango

Traçabilité des Exigences et Vérification par Observateurs pour les Logiciels Critiques des Systèmes Ferroviaires

Ces dernières années, le monde des systèmes critiques a connu un véritable essor en matière de demande de logiciels. Dans une optique majeure de réduction des coûts de développement, les grands acteurs du monde critique comme ceux de l’avionique et de l’automobile s’orientent de plus en plus vers l’ingénierie dirigée par les modèles. Par contre les acteurs du domaine ferroviaire, pour des raisons stratégiques et organisationnelles restent encore fidèles à des méthodes conventionnelles qui leur permettent de tirer au maximum profit de leurs compétences. Cependant, ces approches conventionnelles souffrent d’un manque d’abstraction pour la traçabilité des préoccupations et la vérification formelle, qui sont fortement recommandées, voire obligatoires, dans le développement des logiciels critiques dans le domaine ferroviaire. Pour faire face à ces limitations, nous présentons dans cette thèse une approche systématique basée sur l’ingénierie dirigée par les modèles à base de composants, de façon à maîtriser au mieux la complexité des logiciels et la traçabilité des préoccupations. Nous proposons notamment trois contributions essentielles. En premier lieu, nous fournissons un ensemble uniformisé de méta-modèles permettant de décrire les préoccupations des exigences logicielles, les composants logiciels, et la traçabilité entre les préoccupations et ces composants logiciels. Avec la deuxième contribution, nous proposons un support formel de notre modèle pour en permettre la vérification formelle. Finalement, la dernière contribution propose une approche de développement et de vérification à base de composants logiciels, nommée SARA pour « SAfety-critical RAilway control applications ». Les expérimentations conduites pour évaluer notre approche à partir de quelques cas d’études du nouveau système européen de contrôle de train ERTMS/ETCS, montrent qu’en utilisant des modèles à base de composants qui intègrent explicitement la traçabilité des exigences, nous sommes capables de fournir une approche pratique, extensible et fiable.

Jury

- Directeur(s) de thèse : Laurence DUCHIEN et Christophe GRANSART - Rapporteurs : Jean-Charles Fabre et Philippe Dhaussy - Examinateurs : Franck Barbier et Simon Collart-Dutilleul - Invité : Yannick Moy

Thesis of the team Spirals defended on 18/09/2015