Asfand YAR

Résumé

Aujourd’hui, les systèmes logiciels constituent l’épine dorsale sur laquelle repose l’industrie ferroviaire. Ils permettent d'atteindre un haut niveau d'automatisation qui augmente le niveau de performance global des mécanismes ferroviaires et conduit à de nouvelles générations de systèmes comme les systèmes autonomes. Plusieurs projets dotés de financements importants sont ainsi consacrés partout dans le monde à la production rigoureuse de ces systèmes logiciels tout au long de leur processus de développement. En effet, les systèmes ferroviaires doivent satisfaire à des exigences de sécurité pour être certifiés et rendus opérationnels. Dans ce contexte, l’une des exigences majeures abordées par la plupart des travaux de recherche dans ce domaine est la correction, ce qui signifie qu’un système ferroviaire ne doit pas engendrer des accidents. Cette exigence est aujourd'hui bien maîtrisée grâce aux méthodes formelles qui permettent de définir un système logiciel à l'aide de notations mathématiques assistées par des outils de raisonnement automatisé comme des prouveurs, des solveurs de contraintes, ou des model-checkers. En effet, on peut citer plusieurs exemples réussis d'application de méthodes formelles dans le domaine ferroviaire, comme l'application de la méthode B pour l'automatisation du métro parisien. Par conséquent, l’application de méthodes formelles devient vitale pour ces systèmes. Cependant, les notations formelles ne sont pas faciles à comprendre par tous les acteurs impliqués dans le processus de développement car elles nécessitent de bonnes compétences en mathématiques. Parmi ces acteurs, on rencontre des agents territoriaux, des juristes, des autorités de certification, etc., qui n'ont pas la formation mathématique nécessaire à la prise en main de ces méthodes. Cela pose des problèmes de validation car même si un système ferroviaire est prouvé à l'aide de méthodes formelles, il n’est pas garanti qu'il soit correct vis-à-vis des exigences métier.
Afin de surmonter ces défis, cette thèse propose un cadre formel basé sur des DSLs qui combine des méthodes formelles avec des représentations spécifiques du domaine. En effet, les représentations spécifiques à un domaine aident à la validation et à l'acceptation par les experts du domaine car elles sont censées être plus significatives (d'un point de vue humain) qu'une spécification formelle ; et ce, en particulier pour les acteurs qui ne sont pas familiers avec les notations formelles. Les représentations spécifiques (textuelles ou graphiques) des concepts du domaine sont très utilisées grâce à leur capacité à présenter des informations standardisées des mécanismes ferroviaires : voies, règles et systèmes d'enclenchement. Dans notre cadre, le DSL ferroviaire est basé sur des notations ferroviaires standards comme EULYNX, et sa sémantique est définie à l'aide de la méthode formelle B. Ce cadre prend également en charge l'exécution du DSL ferroviaire avec la sémantique dynamique fournie par des spécifications ERTMS/ETCS B ayant déjà été prouvées. Ces spécifications B sont connectées à la sémantique du DSL à l’aide d’une spécification de liaison, elle-même écrite en B. L'utilisation d'EULYNX et d'ERTMS/ETCS dans le DSL rend les modèles ferroviaires conformes aux normes. L'exécution et la traduction de la sémantique du DSL en B est prise en charge par Meeduse. Il s'agit d'un environnement dédié à l'instrumentation formelle des DSL à l'aide de la méthode B. Il est construit au dessus de Eclipse Modeling Framework et ProB, fournissant des fonctionnalités de vérification, d'animation et de déboggage.