Dans le domaine industriel, la validation des logiciels et des systèmes critiques représente une part significative du coût de développement, notamment lorsqu’elle fait appel à des démarches manuelles d’analyse, de test ou d’audit, où la qualité du produit dépend directement de l’effort de validation fourni. Or, les outils mathématiques des méthodes dites « formelles » rendent possibles l’automatisation partielle du processus, et peuvent modifier l’approche de validation, par exemple en remplaçant des campagnes de tests exhaustives par des méthodes analytiques.
Qu’appelle-t-on « méthodes formelles » ? Ce sont des techniques de conception et d’analyse de logiciels ou de systèmes (spécifications, schémas de conception, données, code) basées sur des théories mathématiques algébriques qui permettent de valider des propriétés importantes sur ces systèmes et logiciels. La mise en œuvre de ces solutions mathématiques requiert cependant la compréhension de leur cadre d’usage mais aussi la maîtrise d’outils logiciels d’analyse, de preuve, etc.
L’Institut CEA-List de CEA Tech développe depuis de nombreuses années ces techniques et ces outils au bénéfice des industriels dans les domaines critiques de l’énergie, de l’aéronautique, du naval, du ferroviaire, mais aussi dans le domaine de la robotique médicale (notamment pour les recherches avancées conduites à Clinatec), ou celui de la sécurité logicielle. Elles apportent une sécurité de fonctionnement renforcée et permettent de raccourcir les délais de développement du logiciel.
Pour Marko Erman, Senior Vice-Président, Directeur technique de Thales : « La relation directe entre la complexité croissante des systèmes et l’augmentation des coûts de développement rend cruciale l’innovation, y compris dans les phases de vérification et de validation. Ce laboratoire commun avec CEA Tech permettra à Thales d’accélérer le déploiement des méthodes formelles dans le groupe, avec pour objectif d’améliorer la performance de l’ingénierie ».
Jean Therme, Directeur de CEA Tech, se félicite également de ce rapprochement : « Le CEA-List a construit une expertise dans l’application des approches formelles dans différents domaines industriels ; nous sommes heureux aujourd’hui d’en faire bénéficier notre partenaire Thales dans son processus de validation des systèmes critiques ».