Analyse et validation formelle de logiciels

CLEARSY propose une méthode d’analyse inédite permettant de faire la preuve mathématique de la conformité de tout ou partie d’un logiciel vis-à-vis d’un besoin fonctionnel et de sécurité.

• Télécharger la plaquette pdf d’analyse formelle de logiciels

L’activité d’analyse que nous proposons établit un lien formel direct entre le code source et les propriétés définies pour le système qui intègre le logiciel. Cette activité permet de détecter tout type de non-conformité ayant pu être introduite dans le cycle de développement : depuis la pensée des algorithmes identifiés en phase de définition système, jusqu’à leur réalisation concrète en tenant compte des éventuelles contraintes spécifiques d’implémentation.

L’activité d’analyse formelle proposée par CLEARSY est complète : elle garantit de couvrir tous les cas de fonctionnement possible, incluant de fait tous les dysfonctionnements et toutes les pannes (du système) qui n’ont pas été explicitement écartées. C’est le bénéfice de l’emploi d’une méthode basée sur les mathématiques et une approche par propriété, et non une approche basée par cas.

Intérêt industriel

Les bénéfices d’une telle analyse formelle sont variés :

• Consolider ou mettre à plat les besoins fonctionnels et de sécurité : expliciter ce que le système doit garantir.
• Identifier des non conformités : des non-respects de propriété pouvant avoir de lourdes conséquences sur la sécurité ou sur l’exploitation du système intégrant le logiciel.
• Retrouver les raisonnements initiaux : ceux imaginés par les concepteurs du système.
• Mettre à plat les choix de conception : en retrouvant leur raison profonde, garantissant la maitrise complète du logiciel étudié.
• Identifier des nœuds de complexité inutiles ou obsolètes : pour simplifier le logiciel et obtenir un gain de performance ainsi que des améliorations fonctionnelles (plus le logiciel est simple, plus il a des chances de bien fonctionner).

Des résultats projets concrets et rapides

La méthode peut s’appliquer de manière rétroactive sur un logiciel existant. Elle gagne également à être pérennisée dans un processus industriel traditionnel, pour déplacer l’effort d’analyse vers les phases amonts du développement et détecter les erreurs au plus tôt pour limiter la boucle de correction (et les tests à refaire).

La méthode se veut pragmatique pour des résultats projets concrets et rapides. Les résultats obtenus ont permis à CLEARSY d’obtenir la garantie que l’activité d’analyse formelle de logiciel représente un réel intérêt industriel tant pour le fournisseur du produit que pour son exploitant. Elle gagne à être utilisée sur des produits qui évoluent régulièrement dans le temps, ou largement déployés ou qui intègrent des options en fonction de leur utilisation.

Références commerciales