Quels sont les obstacles qui empêchent l'adoption généralisée de méthodes formelles? [fermé]

Les méthodes formelles peuvent être utilisées pour spécifier, prouver et générer du code pour une application. Ceci est moins sujet aux erreurs - donc principalement utilisé dans les programmes de sécurité / critiques.

Pourquoi ne l'utilisons-nous pas plus souvent pour la programmation de tous les jours, ou dans des applications web, etc ...?

Les références :

• Méthodes formelles
• Méthode B
• Hoare Logic

Un ingénieur est une personne qui peut faire avec un dollar ce que n'importe quel idiot peut faire avec 10.

Contraintes de ressources, contraintes budgétaires, contraintes de temps, elles sont toutes importantes.

Le développement de logiciels utilisant des méthodes formelles est généralement beaucoup plus cher et prend beaucoup plus de temps que sans. De plus, pour de nombreux projets, la partie la plus difficile est de comprendre les exigences commerciales. Tout ce que l'utilisation de méthodes formelles vous achète dans ce cas est la preuve que votre code correspond à 100% à votre compréhension incomplète et incorrecte des exigences commerciales.

Pour cette raison, l'utilisation de méthodes formelles, de preuves, de vérification de programme et de techniques similaires est généralement limitée aux "choses qui comptent", à savoir les logiciels avioniques, les systèmes de contrôle pour les équipements médicaux, les centrales électriques, etc.

Programmer ou ne pas programmer?

Pour résoudre un problème avec un produit logiciel, après avoir une bonne compréhension des exigences, vous pouvez SOIT écrire un programme en utilisant les langages de programmation OU spécifier le programme à l' aide d' un langage formel des outils et la génération de code d'utilisation. Ce dernier ajoute juste un niveau d'abstraction.

Faire les choses correctement ou faire les bonnes choses?

L'approche formelle vous donne la preuve que votre logiciel fonctionne selon les spécifications. Votre produit fait donc les choses correctement. Mais fait-il les bonnes choses?

Les exigences sur lesquelles vous travaillez peuvent être incomplètes ou ambiguës. Ils pourraient même être bogués. Dans le pire des cas, les besoins réels ne sont même pas exprimés. Mais une image vaut mille mots, juste des images google pour "Ce que veut le client", par exemple de cet article :

Le coût de la formalité

Dans un monde parfait, vous auriez des exigences parfaitement détaillées et parfaites dès le départ. Vous pouvez alors spécifier entièrement votre logiciel. Si vous optez pour le formel, votre code serait généré automatiquement afin que vous soyez plus productif. Les gains de productivité compenseraient le coût des outils formels. Et tout le monde utiliserait désormais des méthodes formelles. Alors pourquoi pas?

En pratique, c'est rarement la réalité! C'est pourquoi tant de projets en cascade ont échoué, et pourquoi les méthodes de développement itératives (agile, RAD, etc.) ont pris les devants: elles peuvent gérer des exigences, des conceptions et des implémentations incomplètes et imparfaites et les affiner jusqu'à ce qu'elles soient fines.

Et voici le point. Avec les méthodes formelles, chaque itération nécessite d'avoir une spécification formelle complètement cohérente. Cela nécessite une réflexion approfondie et un travail supplémentaire, car la logique formelle ne pardonne pas et n'aime pas les pensées incomplètes. Les expériences simples à jeter deviennent coûteuses sous cette contrainte. Et il en va de même pour chaque itération qui entraînerait un retour en arrière (par exemple, une idée qui n'a pas fonctionné ou une exigence qui a été mal comprise).

En pratique

Lorsque vous n'êtes pas obligé d'utiliser des méthodes formelles pour des raisons juridiques ou contractuelles, vous pouvez également atteindre une très haute qualité sans systèmes formels, par exemple en utilisant une programmation basée sur des contrats et d'autres bonnes pratiques (par exemple, révision de code, TDD , etc.). Vous ne pourrez pas prouver que votre logiciel fonctionne, mais vos utilisateurs apprécieront le logiciel plus tôt.

Mise à jour: effort mesuré

Dans le numéro d'octobre 2018 de Communications of the ACM, il y a un article intéressant sur les logiciels officiellement vérifiés dans le monde réel avec quelques estimations de l'effort.

Fait intéressant (basé sur le développement de systèmes d'exploitation pour les équipements militaires), il semble que la production de logiciels officiellement éprouvés nécessite 3,3 fois plus d'efforts qu'avec les techniques d'ingénierie traditionnelles. C'est donc très coûteux.

D'un autre côté, cela nécessite 2,3 fois moins d'efforts pour obtenir des logiciels de haute sécurité de cette façon qu'avec les logiciels de conception traditionnelle si vous ajoutez l'effort de rendre ces logiciels certifiés à un niveau de sécurité élevé (EAL 7). Donc, si vous avez des exigences élevées en matière de fiabilité ou de sécurité, il y a définitivement un intérêt à devenir formel.

La conception et le développement du code seL4 ont pris deux années-personnes. L'addition de toutes les preuves sérospécifiques au fil des ans représente un total de 18 années-personnes pour 8 700 lignes de code C. En comparaison, L4Ka :: Pistachio, un autre micro-noyau de la famille L4, de taille comparable à seL4, a pris six années-personnes pour se développer et ne fournit aucun niveau d'assurance significatif. Cela signifie qu'il n'y a qu'un facteur 3,3 entre les logiciels vérifiés et les logiciels de conception traditionnelle. Selon la méthode d'estimation de Colbert et Boehm 8, une certification EAL7 selon les Critères communs traditionnels pour 8 700 lignes de code C prendrait plus de 45,9 années-personnes. Cela signifie que la vérification formelle de l'implémentation au niveau binaire est déjà plus d'un facteur de 2,3 moins coûteux que le niveau de certification le plus élevé des Critères communs, tout en offrant une assurance nettement plus solide.

Chaque programme dans n'importe quelle langue peut être considéré comme une spécification formelle (équivalente à une machine à tourner). Toute «spécification formelle» de niveau supérieur à utiliser pour prouver l'exactitude formelle est également - juste un autre programme. Mais c'est (typiquement) un programme mauvais, incomplet, vague, insuffisamment réfléchi. Et ce n'est pas un hasard, généralement écrit par des personnes qui ne savent pas programmer (ce sont généralement des experts du domaine).

Et donc prouver qu'un programme est compatible (produit les mêmes réponses ou selon la façon dont vous le caractérisez) avec ses exigences formelles de niveau supérieur, invariable se résume à la façon dont vous résolvez les ambiguïtés dans la spécification formelle de niveau supérieur. Il n'y a pas de bonne manière générale de le faire.

Cette mise en correspondance des exigences de haut niveau avec les détails de niveau inférieur est l'essentiel de la véritable programmation. Il ne devrait pas être surprenant que le travail de base effectué par un programmeur lisant et interprétant des spécifications ne puisse pas être remplacé par un geste de la main et en disant `` maintenant, juste voir si cette spécification formelle de haut niveau est respectée par cet exemple de programme ''.

Même aux premiers jours de la programmation logique, où ce concept semblait à première vue si prometteur (car à la fois la spécification de haut niveau et les programmes sous-jacents réels pouvaient être écrits dans le même langage), ce problème central s'est avéré insoluble.