SPaCIFY Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vol spatiaux – SPaCIFY

Le projet SPaCIFY s’inscrit dans un mouvement destiné à augmenter de façon drastique la qualité et l’étendue des fonctionnalités des logiciels de vol (LV), tout en abaissant leurs coûts et durées de développement. La disponibilité d’un environnement de conception adapté au métier spatial constitue une des réponses à cette problématique. Il n’en existe pas à l’heure actuelle : le projet SPaCIFY consiste précisément à définir un tel atelier, sous forme de logiciel libre afin notamment d’en assurer la pérennité. L’atelier met en oeuvre une méthodologie de conception de logiciels spatiaux répondant à des exigences de haute fiabilité et de criticité et à des contraintes temporelles et physiques spécifiques. Il s’appuie sur des concepts existants, éprouvés en particulier dans l’aéronautique, pour en accroître les caractéristiques majeures et les instancier pour le domaine spatial. La structure de l’atelier est articulée autour d’un modèle de calcul synchrone multi-horloge, pour lequel seront définis un langage de modélisation et des méthodes et procédés de conception, afin d’améliorer le développement des logiciels de vol spatiaux. La méthodologie envisagée consiste à mettre en oeuvre des techniques d’ingénierie des modèles, sur des modèles dotés d’unesémantique formelle. Il procède par la définition des procédures de concrétisation ou de raffinement visant à une synthèse automatique et certifiable des fonctionnalités logicielles au moyen d’une part, de techniques de vérification formelle basées sur le « model-checking », d’autre part sur l’utilisation d’assistants de preuve permettant de certifier les étapes de développement. L’originalité principale de l’atelier proposé est son articulation autour du modèle de calcul symbolique polychrone (synchrone multi-horloge). Ceci permet de tenir compte des caractéristiques d’ordonnancement et de répartition du logiciel de manière abstraite (au moyen de relations d’ordre partiel décrivant synchronisations et causalités) tout en facilitant grandement la vérification formelle (en limitant considérablement l’espace des configurations à explorer). Enfin, la spécialisation du projet au domaine du logiciel de vol spatial permettra de concevoir une bibliothèque dédiée de raffinements et de vérifications paramétrés dont la correction sera démontrée formellement dans la plupart des cas. Les logiciels et résultats mis en oeuvre au cours du projet seront livrés sous forme de logiciel libre et intégrés à l’atelier Topcased, porté par Airbus Industries dans le contexte du pôle de compétitivité AESE (Aéronautique, Espace et Systèmes Embarqués).