L’équipe MOSES a pour objectif de développer des méthodes formelles pour la conception et l’exploitation des systèmes à événements discrets (SED), sûrs de fonctionnement. Nous utilisons des formalismes tels que les réseaux de Petri ou les automates, pour construire des modèles de systèmes selon différents niveaux d’abstractions et les objectifs de commande ou supervision. Notre objectif est de développer des méthodes d’ingénierie adaptées à la commande des SED critique, en nous basant sur l’ingénierie système et la vérification formelle. Ces méthodes doivent permettre la construction assistée par transformation de modèles, des modèles formels pour la commande et le diagnostic. Les techniques de vérifications formelles comme le model-checking ou le theorem proving permettent de réduire les coûts de conception par la vérification rapide des propriétés du système et sa validation. Ces méthodes doivent également permettre la génération automatique des tests unitaires et d’intégration. Associées à la vérification formelle, elles doivent également permettre l’utilisation de composants sur étagères pour la réduction des coûts de développement de SED critiques. Dans ce cadre, l’explosion combinatoire est l’un des principaux verrous que nos méthodes doivent combattre. L’utilisation de formalismes avec un haut niveau d’expressivité (Automates temporisés, Réseaux de Petri temporel ou temporisés …) et l’utilisation des techniques modulaires ou distribuées sont des moyens et techniques que nous développons pour proposer des solutions qui soient scalables. Au niveau applicatif, notre ambition est de transférer l’expérience acquise dans la conception des systèmes manufacturiers, vers la conception de systèmes embarqués critiques. Nous nous intéressons plus particulièrement (mais sans exclusivité) au contrôle et à la signalisation ferroviaire du futur. En effet, une partie de notre stratégie est liée à notre participation active, à l’IRT RAILENIUM. Ainsi, nous développons UNIRAIL, une plateforme ferroviaire servant de benchmark. C’est une plate-forme de tests ouverte qui permettra de tester différents systèmes de contrôle et signalisation ferroviaire. Ainsi UNIRAIL est conforme au système européen de gestion du trafic ferroviaire (ERTMS) et permettra de développer les modèles et algorithmes pour la commande automatique des trains.