Comment créer un logiciel essentiel à la mission?

Je suis des méthodes formelles d'auto-apprentissage. J'ai entendu dire que des méthodes formelles sont utilisées (et généralement uniquement utilisées) pour créer des logiciels essentiels à la mission (tels que le contrôleur de réacteur nucléaire, le contrôleur de vol d'avion, le contrôleur de sonde spatiale). C'est pourquoi je suis intéressé à l'apprendre: p

Cependant, après avoir appris des méthodes formelles (en particulier LTL, CTL et leurs frères et sœurs), je pense qu'elles ne peuvent être utilisées que pour vérifier l'exactitude de la spécification (sécurité, vivacité, équité, etc.).

Mais alors comment vérifier que le logiciel (pas seulement la spécification) est bien correct?

Avertissement: je suis un idiot à 90% en matière d'informatique théorique. Veuillez donc être miséricordieux en répondant.

La question est assez large. Pour y répondre dans un espace raisonnable je ferai de nombreuses simplifications excessives.

Entendons-nous sur la terminologie. Un programme est correct lorsqu'il implique sa spécification. Cette vague déclaration est rendue précise à bien des égards, en épinglant exactement ce qu'est un programme et ce qui est exactement une spécification. Par exemple, dans la vérification des modèles, le programme est une structure Kripke et la spécification est souvent une formule LTL . Ou, le programme pourrait être une liste d'instructions PowerPC et la spécification pourrait être un ensemble d' assertions Hoare-Floyd écrites, disons, dans une logique de premier ordre. Il existe de très nombreuses variantes possibles. Il est tentant de conclure que dans un cas (structure Kripke) nous ne vérifions pas un programme réel, tandis que dans le second cas (liste d'instructions PowerPC) nous le faisons. Cependant, il est important de réaliser que nous examinons vraiment des modèles mathématiques dans les deux cas, et c'est parfaitement bien. (La situation est assez similaire à la physique où, par exemple, la mécanique classique est un modèle mathématique de la réalité.)

La plupart des formalisations distinguent la syntaxe et la sémantique d'un programme; c'est-à-dire, comment il est représenté et qu'est-ce que cela signifie. La sémantique d'un programme est ce qui compte du point de vue de la vérification du programme. Mais, il est bien sûr important d'avoir une manière claire d'attribuer des significations aux (représentations syntaxiques des) programmes. Deux méthodes populaires sont les suivantes:

• (petite étape) sémantique opérationnelle : Cela ressemble beaucoup à la définition d'un langage de programmation en lui écrivant un interpréteur. Pour cela, vous devez dire quel est l' état , et il est affecté par chaque déclaration dans la langue. (Vous vous demandez peut-être dans quelle langue vous écrivez l'interprète, mais je vais prétendre que vous ne l'êtes pas.)
• sémantique axiomatique : Ici, chaque type d'instruction est accompagné d'un schéma axiomatique . Donc, à peu près, chaque fois qu'une instruction particulière de ce type est utilisée, cela se traduit par la possibilité d'utiliser certains axiomes. Par exemple, l'affectation est fournie avec le schéma ; l'affectation particulière est accompagnée de l'axiome si nous instancions le schéma avec . { P [ x / e ] ${\bf x}:={\bf e}$x : = x + 1 { x + 1 = 1 $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$$x:=x+1$P = ( x = 1 $\{x+1=1\}\,x:=x+1\,\{x=1\}$$P=(x=1)$

(Il y en a d'autres. Je me sens particulièrement mal d'avoir omis la sémantique dénotationnelle, mais cette réponse est déjà longue.) Le code machine plus la sémantique opérationnelle est assez proche de ce que la plupart des gens appellent un «vrai programme». Voici un papier séminal, qui se trouve utiliser la sémantique opérationnelle pour un sous-ensemble du code machine DEC Alpha:

• Necula, Lee, Proof-Carrying Code , 1996

Pourquoi voudriez-vous jamais utiliser une sémantique de niveau supérieur, comme celle sémantique axiomatique? Lorsque vous ne souhaitez pas que votre preuve d'exactitude dépende du matériel sur lequel vous exécutez. L'approche consiste alors à prouver l'exactitude d'un algorithme par rapport à une sémantique de haut niveau pratique, puis à prouver que la sémantique sonne par rapport à une sémantique de niveau inférieur qui est plus proche des machines réelles.

En résumé, je pourrais penser à trois raisons qui ont conduit à votre question:

1. Vous n'avez vu que des sémantiques de haut niveau qui ne ressemblent pas à ce que vous appelez un programme, et vous vous demandez s'il y en a de bas niveau. La réponse est oui.
2. Vous vous demandez comment vous prouvez qu'un modèle correspond à la réalité. Comme en physique, non. Il vous suffit de trouver de meilleurs modèles et de les comparer à la réalité.
3. Vous n'avez pas vu la distinction entre la syntaxe et la sémantique, et diverses façons d'attribuer des significations aux programmes. Deux questions précédentes énumèrent quelques livres.

Cette réponse essaie simplement d'identifier trois façons différentes dont j'ai compris la question. Aller en profondeur dans l' un de ces points nécessiterait beaucoup d'espace.

Une approche pour réduire l'écart entre un programme et sa spécification consiste à utiliser un langage avec une sémantique formelle. Un exemple intéressant serait ici Esterel . Jetez un coup d'œil à la page Web de Gérard Berry pour des discussions intéressantes sur son travail qui introduit des méthodes formelles dans le monde réel. http://www-sop.inria.fr/members/Gerard.Berry/

ps Été sur un Airbus? Vous avez volé avec des méthodes formelles!

La science de la construction de logiciels fiables dans le «monde réel» est toujours en cours de développement et frôle dans une certaine mesure une étude intrinsèquement culturelle ou anthropologique, car les ordinateurs et les logiciels ne «provoquent» pas de bugs - les humains le font! cette réponse se concentrera sur les approches générales de Q / A dont la vérification formelle du logiciel peut être considérée comme un élément.

une observation remarquable est que, souvent, un logiciel «assez bon» mais «bogué» peut souvent surpasser les logiciels mieux testés mais de moindre fonctionnalité sur le marché. en d'autres termes, le marché n'accorde pas toujours la priorité à la qualité des logiciels et les techniques modernes de génie logiciel, qui ne mettent pas toujours l'accent sur la qualité, reflètent quelque peu cela. de plus, la qualité peut souvent ajouter une dépense importante au produit final. avec ces mises en garde, voici quelques éléments de base:

• systèmes redondants / tolérants aux pannes. il s'agit d'un vaste domaine d'étude. la tolérance aux pannes et la redondance peuvent être conçues dans les nombreuses couches d'un système. par exemple un routeur, un serveur, un lecteur de disque, etc.

• test . tous les types: tests unitaires, tests d'intégration, tests d'acceptation des utilisateurs, tests de régression, etc.

• de nos jours, les tests automatisés via des suites de tests qui peuvent être exécutés sans surveillance sont plus développés / importants. les suites de tests en cours d'exécution sont souvent associées à l'outil de génération.

• un concept important dans les tests est la couverture du code . c'est-à-dire quel code est exercé par le test. un test ne peut pas trouver un bogue dans le code qui n'est pas "touché" par le test.

• un autre concept clé dans les tests est le harnais de test qui exerce un code qui n'est pas facilement accessible directement.

• les tests doivent exercer tous les niveaux du logiciel. si le logiciel est bien modulaire, ce n'est pas difficile. les tests de niveau supérieur devraient pénétrer profondément dans le code. les tests qui exercent de grandes quantités de code avec une petite configuration de test augmentent le «levier de test» .

• rendre le code le moins compliqué possible est important pour les tests. les tests doivent être pris en compte dans la conception de l'architecture. il existe souvent plusieurs façons d'implémenter la même fonctionnalité, mais certaines ont des implications très différentes pour la couverture / l'effet de levier des tests. pour chaque branche du code, c'est souvent un autre cas de test. les branches au sein des branches dégénèrent en une augmentation exponentielle des chemins de code. donc éviter la logique hautement imbriquée / conditionnelle améliore la capacité de test.

• étudier les pannes de logiciels célèbres (massives), dont il existe de nombreux exemples et études de cas, est utile pour comprendre l'histoire et développer un état d'esprit orienté vers des considérations de qualité.

• on peut se laisser emporter par les tests! il y a à la fois un problème avec trop peu ou trop de tests. il y a un "sweet spot". le logiciel ne peut pas être construit avec succès dans les deux extrêmes.

• utiliser tous les outils de base de la manière la plus efficace. débogueurs, profileurs de code, outils de couverture de code de test, système de suivi des défauts, etc.! ne vous engagez pas nécessairement à réparer, mais suivez même les plus petits défauts du logiciel de suivi.

• une utilisation prudente de SCM, de la gestion du code source et des techniques de branchement est importante pour éviter les régressions, isoler et progresser les correctifs, etc.

• Programmation en version N : une pratique souvent utilisée pour développer des logiciels essentiels à la mission. Le principe de cette pratique est qu'il est peu probable que N programmes développés indépendamment aient le même bug / défaut commun. Cela a été critiqué dans quelques articles . La NVP n'est cependant pas un concept théorique.

Je crois que le physicien Feynman a un certain compte rendu de la méthode utilisée par la NASA pour garantir la fiabilité des systèmes de navette spatiale dans son livre "Qu'est-ce que vous pensez de ce que les autres pensent?" - il a dit qu'ils avaient deux équipes, disent l'équipe A et l'équipe B. l'équipe A a construit le logiciel. l'équipe B a adopté une approche contradictoire avec l'équipe A et a tenté de casser le logiciel.

cela aide si l'équipe B a une bonne formation en génie logiciel, c'est-à-dire qu'elle peut elle-même écrire des tests de programmation / tests de programmation, etc. dans ce cas, l'équipe B avait un niveau de ressources presque égal à l'équipe A. en revanche, cette approche est coûteuse car elle peut presque doubler le coût de construction du logiciel. plus généralement, l'équipe de contrôle qualité est plus petite que l'équipe de développement.

Une ancienne approche (mais elle est toujours utilisée dans certaines applications) est la programmation en version N

De Wikipédia:

La programmation en version N ( NVP ), également connue sous le nom de programmation multiversionnelle , est une méthode ou un processus en génie logiciel où plusieurs programmes fonctionnellement équivalents sont générés indépendamment à partir des mêmes spécifications initiales. Le concept de programmation en version N a été introduit en 1977 par Liming Chen et Algirdas Avizienis avec la conjecture centrale que "l'indépendance des efforts de programmation réduira considérablement la probabilité que des erreurs logicielles identiques se produisent dans deux ou plusieurs versions du programme". de NVP est d'améliorer la fiabilité du fonctionnement du logiciel en intégrant la tolérance aux pannes ou la redondance.
....

Voir par exemple: " Défis liés aux défauts de construction - Système de commande de vol tolérant pour un aéronef civil "

fajrian, cette question que vous avez posée couvre deux des plus gros problèmes de la recherche d'ingénieur logiciel: la conformité entre la spécification et le modèle et entre le modèle et le code. Modélisez ici une représentation de ce que le système va faire, ou comment il sera fait, il y a beaucoup de niveaux pour modéliser un système.

Donc, il y a des gens qui essaient de trouver la meilleure réponse à votre question. Parce qu'il est très difficile de vérifier l'exactitude d'un logiciel basé sur un modèle, par exemple, en utilisant des méthodes formelles. Je sais que JML est un moyen de le faire, mais je ne connais pas les limites de son utilisation.

Pour conclure, combien il est difficile de vérifier l'exactitude du code, les gens essaient de mélanger les méthodes formelles et les tests, créant des tests automatiquement à partir des spécifications par exemple. Un exemple pour les systèmes en temps réel est le TIOSTS qui est basé sur des événements temporisés d'entrée / sortie.

Le test n'est pas seulement une approche de méthode formelle, cela améliore la fiabilité mais ne vérifie pas l'exactitude.

Il y a deux ou trois ans, j'ai commencé à me pencher sur les méthodes formelles appliquées aux logiciels. C'était une quête motivée par la curiosité et par le sentiment que je devais apprendre des outils et des méthodes de programmation avec des délais plus longs. Même si je rêvais d'un Silver Bullet , je pensais vraiment qu'il n'y avait pas de réponse à la question: "Comment puis-je écrire un programme correct?".

À ce stade de la quête, après avoir essayé certains outils (Z, B, VHDL et Estelle), j'utilise TLA + . Il s'agit d'une variante de la logique temporelle avec des outils logiciels pour la vérification des modèles et les preuves mécaniques. Je pense que j'ai choisi cette approche parce que L. Lamport était derrière, la syntaxe était simple, il y avait beaucoup d'exemples, il y avait une communauté qui s'en occupait, et le langage et les outils étaient assez bien documentés.

Concernant ma question initiale, je pense qu'il n'y a pas de réponse complète. Cependant, il vaut la peine d'apprendre qu'il vaut la peine de spécifier formellement certaines parties d'un système. Il est également très utile de désosser certains complexes. Autrement dit, il est efficace de créer un plan pour les parties difficiles et critiques. Cependant, je ne pense pas qu'il existe une méthode efficace pour traduire automatiquement la spécification dans un langage de programmation ou un framework (sauf si vous limitez le projet à un environnement très spécifique). Je ne pense pas non plus qu'avoir une spécification formelle devrait vous empêcher de tester le logiciel.

En un mot, je pense que la métaphore suivante (de Lamport) est vraiment puissante: "Vous attendez-vous à ce qu'une maison soit automatiquement construite à partir d'un plan? Achèterez-vous une maison qui n'est pas encore construite et qui n'a pas de plan?" .

Au cours de cette quête, j'ai trouvé les ressources suivantes utiles:

• Méthodes de spécification du logiciel . Ce livre offre un large aperçu des méthodes et outils existants. Vous y trouverez des explications de base et des exemples de Z, SDL, TLA +, Petri Nets, Coq, etc.
• Si vous pensez que TLA + répond à vos besoins, je recommande vraiment le livre Specifying Systems . Vous pouvez obtenir le livre gratuitement, et il est livré avec des exemples pour jouer avec :).
• Récemment, j'ai lu quelques articles connexes qui donnent deux perspectives différentes sur l'état de l'art des méthodes formelles: le cas des méthodes formelles et les mathématiques formellement vérifiées .

Bonne chance!

Jusqu'à présent, les réponses couvraient déjà la majeure partie de ce qui devrait être dit sur les fondements de la relation entre la spécification et le code. Je veux juste ajouter un point plus pratique qui aborde la question dans l'en-tête de ce fil:

Comment créer un logiciel critique?

Il existe des outils qui analysent automatiquement votre code pour détecter les erreurs (violations de la spécification ou "bogues typiques"). À ma connaissance, ces méthodes s'appuient principalement sur l'analyse statique et ne sont pas immédiatement liées aux théories que vous avez mentionnées (LTL / CTL / ...), mais elles trouvent des erreurs dans le code réel et c'est déjà faisable, d'un point de vue pratique. d’utiliser ces outils dans des projets industriels. Personnellement, je n'en ai pas utilisé beaucoup, mais il semble que ces outils commencent à être acceptés par les pratiquants. Pour plus de lecture, je peux recommander l'article de blog suivant:

http://www.altdevblogaday.com/2011/12/24/static-code-analysis/

Les algorithmes de certification peuvent être utiles lors de la création de logiciels critiques.

Un algorithme de certification est un algorithme qui produit, avec chaque sortie, un certi fi cat ou un témoin (preuve facile à vérifier) ​​que la sortie particulière n'a pas été compromise par un bogue.

Pour en savoir plus, consultez ce document d'enquête Algorithmes de certification de McConnell, RM et Mehlhorn, K. et Naher, S. et Schweitzer, P.

Mais alors comment vérifier que le logiciel (pas seulement la spécification) est bien correct?

Tests unitaires? Écrivez un test pour chaque exigence de la spécification, puis testez chaque méthode de votre implémentation pour vérifier que sa sortie / entrée est conforme à ladite spécification. Cela peut être automatisé afin que ces tests soient exécutés en continu pour garantir qu'aucun changement n'interrompt jamais les fonctionnalités qui fonctionnaient auparavant.

Théoriquement, si vos tests unitaires ont une couverture de code à 100% (c'est-à-dire que chaque méthode de votre code est testée), votre logiciel doit être correct, à condition que les tests eux-mêmes soient précis et réalistes.