Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Final macsi 1 C Introduction C ? est une méthode de spéci ?cation formelle qui permet gr? ce à un langage adéquat d ? exprimer très rigoureusement les propriétés exigées dans un cahier des charges Il est alors possible de prouver de manière automatisée qu

C Introduction C ? est une méthode de spéci ?cation formelle qui permet gr? ce à un langage adéquat d ? exprimer très rigoureusement les propriétés exigées dans un cahier des charges Il est alors possible de prouver de manière automatisée que ces propriétés sont non ambigu? s cohérentes et non contradictoires Cela nous permet de garantir ensuite par preuve mathématique que ces propriétés sont respectées au fur et à mesure des étapes de conception Ainsi cette méthode formelle et la preuve qui lui est associée permettent ?? D ? obtenir des spéci ?cations techniques et des cahiers des charges système clairs structurés cohérents et sans ambigu? té ?? De développer des logiciels garantis contractuellement sans défauts Dans des domaines tels que le temps réel les automatismes industriels les protocoles de communication les protocoles cryptographiques l ? informatique embarquée ? La méthode formelle B ? évoque traditionnellement l ? ensemble comprenant le langage B le ra ?nement la preuve et les outils associés Un développement B débute par l ? écriture d ? un modèle concret reprenant tous les aspects du besoin Les principales données sont manipulées par le système et sont décrites ainsi que les propriétés fondamentales de ces données Des services assurent les transformations de ces données tout en préservant leurs propriétés Le modèle B ainsi obtenu constitue une spéci ?cation de ce que devra réaliser le système Le modèle B est ensuite transformé ra ?né ? dans le vocabulaire B jusqu ? à obtenir une implantation logicielle complète du logiciel Au ?nal nous aboutissons alors à un modèle concret prouvé et sans défaut transcodable dans le langage C ou Ada La méthode formelle B est donc une démarche de construction prouvée dite correcte sur la base du langage B du ra ?nement et de la preuve ? La méthode B qui n'est pas la seule méthode formelle ni probablement la plus e ?cace sur l'ensemble des aspects rencontrés dans les projets présente des avantages certains sur de nombreux points On dispose d'abord d'une méthode unique pour spéci ?er concevoir et prouver Il n'est donc pas nécessaire de modéliser la spéci ?cation du logiciel pour la prouver une telle modélisation pouvant conduire à des contradictions liées soit à l'interprétation qui en a été faite soit aux limites et aux contraintes du modèle lui-même L'e ?cacité s'est révélée grande pour des modules l'accumulation de nouveaux théorèmes plus performants augmentant le pourcentage de preuves réalisées automatiquement sur un meilleur choix de stratégie de preuve facilitant la preuve sur la réutilisation partielle ou totale de machines sur étagères La garantie par les preuves est sans commune mesure avec le fait de tracer les exigences et d'en véri ?er les transformations successives Le principe même de la preuve intégrée directement dans la conception impose nécessairement une grande rigueur et précision dans l'écriture du langage L'intégration de la qualité à la conception est un atout important On obtient de manière générale un logiciel bien construit et une architecture saine car la preuve se