Méthodes formelles : simplement une bonne pratique d’ingénierie ? (2024)

• Introduction

  • Marc Brooker est un ingénieur chez AWS qui travaille sur les bases de données et les systèmes serverless, et souligne l’importance des méthodes formelles en génie logiciel.

• Importance des méthodes formelles

  • Les méthodes formelles sont essentielles pour faire gagner du temps et réduire les coûts dans les systèmes à grande échelle, les systèmes distribués et les systèmes bas niveau critiques.
  • Le génie logiciel est un exercice d’optimisation du temps et des coûts.
  • Les méthodes formelles réduisent le coût des reprises, traitent plus tôt les changements d’interface et améliorent ainsi la vitesse et l’efficacité du développement logiciel.

• Champ d’application des méthodes formelles

  • La valeur des méthodes formelles peut être limitée pour les logiciels pilotés par des besoins utilisateurs qui évoluent rapidement.
  • Dans les systèmes à grande échelle, distribués et bas niveau, les méthodes formelles réduisent fortement les reprises et la densité de bugs.

• Méthodes formelles et outils

  • Les méthodes formelles et le raisonnement automatisé couvrent divers outils et sont utilisés avec efficacité dans les grands systèmes cloud d’AWS.
  • On y trouve des langages de spécification comme TLA+, P et Alloy, ainsi que des model checkers, des outils de simulation déterministe et des langages de programmation orientés vérification.

• Conclusion

  • Les outils qui aident à réfléchir à l’architecture d’un système dès la phase de conception accélèrent le développement logiciel, réduisent les risques et permettent de concevoir des systèmes optimaux.
  • Pour les ingénieurs qui travaillent sur des systèmes vastes et complexes, les méthodes formelles font partie des bonnes pratiques d’ingénierie.

[GN⁺]

Avis Hacker News

• La vérification formelle des logiciels dépend fortement du type de logiciel et du processus de développement. La plupart des projets logiciels ne sont pas compatibles avec des exigences formelles.

  • Le développement et la conception logiciels avancent souvent en parallèle, ce qui ne convient pas bien aux méthodes formelles.
  • Les systèmes critiques pour la sécurité, comme les logiciels aérospatiaux, peuvent grandement bénéficier de la vérification formelle.

• L’idée que les méthodes formelles peuvent résoudre la complexité logicielle revient souvent.

  • Cela peut séduire les personnes qui privilégient une approche académique.
  • Mais les exemples convaincants montrant comment les méthodes formelles résolvent concrètement les problèmes restent rares.
  • Il est sous-entendu qu’apprendre des outils comme TLA permet de mieux comprendre leur utilité.

• Il existe deux grands types de méthodes formelles : les techniques extrinsèques, séparées du code, et les techniques intrinsèques, intégrées au code.

  • Les techniques intrinsèques opèrent au niveau fonctionnel du code, tandis que les techniques extrinsèques analysent formellement un modèle du code.
  • La recherche sur les méthodes formelles traverse actuellement un âge d’or, et les techniques intrinsèques attirent davantage l’attention.

• Les méthodes formelles légères peuvent être maintenues avec la base de code et offrir plus d’enseignements que les tests unitaires.

  • Cette approche s’accorde bien avec les pratiques habituelles de développement logiciel.

• La vérification formelle des logiciels reste une tâche très difficile et n’a de valeur que dans des cas extrêmes.

  • Elle exige un niveau d’expertise élevé et devient très complexe pour la plupart des systèmes.
  • Des outils comme Lean sont difficiles à apprendre, mais bien documentés.

• De nombreux articles sur les méthodes formelles donnent l’impression de servir surtout à générer des prospects pour des cabinets de conseil.

  • Il faudrait attendre que les méthodes formelles produisent réellement du code de haute qualité.

• Parmi les méthodes formelles légères, on trouve la vérification de traces avec la logique temporelle linéaire (Linear Temporal Logic).

  • C’est une manière simple et puissante d’enregistrer des événements et d’exécuter des conditions sur des traces d’exécution.

• Les méthodes formelles modernes comme TLA+ et Alloy sont aussi faciles à apprendre que Python.

  • De nombreux systèmes cloud ont été vérifiés avec ces outils (par ex. : Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)