Systerel met en œuvre une approche formelle de vérification au travers de SPARK/Ada.
Aujourd’hui, cette dernière est appliquée au secteur ferroviaire (norme EN5018) sur des applications dont la volumétrie oscille entre 20KLOC et 400KLOC.
Les objectifs à atteindre sur ces codes legacy sont de vérifier que :
1. Le flot de données est en accord avec les informations fournies.
2. La sémantique des opérations est en accord avec celle disponible ou exprimée.
3. Le code ne lève pas d’exceptions (AoRTE).
Cette approche vient se greffer à toute la stratégie mise en place par Systerel durant ces 6 dernières années concernant la conduite à tenir sur le portage de legacy Ada.
Mais SPARK/Ada ne s’applique pas qu’à des codes legacy. Cette technologie prend toute son envergure sur des nouveaux développements généralement faits en Ada2012.
Sa mise en œuvre est alors simplifiée et peut se faire avec une courbe d’apprentissage raisonnable.
L’adoption de SPARK contribuera alors sur le long terme :
1. A la qualité structurelle,
2. A la qualité fonctionnelle,
3. A la maintenabilité (Contrats –> oracles de tests),
4. A la satisfaction des exigences Safety et Security,
5. A un esthétisme « technique ».