Méthodes formelles : une simple bonne pratique d’ingénierie ?
Marc Brooker, ingénieur chez Amazon Web Services, soutient dans son discours d’ouverture à la conférence TLA+ que les méthodes formelles ne représentent pas une surcharge coûteuse, mais plutôt un gain de temps et d’argent pour les systèmes critiques de grande envergure, distribués ou de bas niveau. En réduisant les reprises et le coût des modifications, la conception formelle améliore considérablement l’efficacité du développement de logiciels. Tous les logiciels n’en bénéficient pas ; le développement agile est plus adapté aux domaines sensibles aux évolutions des besoins des utilisateurs, comme les interfaces utilisateur ou la logique de tarification. Cependant, pour les grands systèmes aux besoins clairement définis, les méthodes formelles réduisent efficacement le taux de bogues et améliorent les performances. Brooker recommande plusieurs outils, notamment des langages de spécification comme TLA+, P et Alloy, des vérificateurs de modèles et des langages de programmation avec vérification. Il souligne que les méthodes formelles garantissent non seulement la correction, mais aident également à explorer les options d’optimisation, évitant ainsi le compromis difficile entre correction et performance.