Remerciez-le!

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

Toute reproduction sans autorisation du Centre français d’exploitation du droit

Toute reproduction sans autorisation du Centre français d’exploitation du droit de copie est strictement interdite. © Techniques de l’Ingénieur, traité Informatique H 2 550 − 1 Développement et validation de logiciels. Méthodes formelles par Patrick BELLOT Département informatique. École Nationale Supérieure des Télécommunications Jean-Philippe COTTIN Département informatique. École Nationale Supérieure des Télécommunications et Jean-François MONIN France Télécom, Centre National d’Études des Télécommunications, Lannion lors que les ingénieurs électroniciens savent concevoir des matériels qui fonctionnent et que les ingénieurs du bâtiment savent construire des ouvrages qui tiennent, l’ingénieur informaticien semble incapable de produire des applications répondant parfaitement aux besoins qu’elles doivent satisfaire. Quiconque a connu l’industrie de l’informatique sait que lorsqu’une application est produite, il y a un nombre très élevé d’allers et retours entre l’équipe de déve- loppement et les utilisateurs de l’application aﬁn que celle-ci soit modiﬁée. Et même lorsque tout semble satisfaisant, on peut être certain que des problèmes surgiront encore. Les raisons souvent avancées sont le manque de précision ou l’incohérence dans l’expression des besoins des utilisateurs, ce que l’on appelle 1. Généralités................................................................................................. H 2 550 - 2 1.1 Bref historique ............................................................................................. — 2 1.2 Niveaux d’utilisation des méthodes formelles.......................................... — 3 2. Méthodes formelles et cycle de vie du logiciel............................... — 3 3. Bases mathématiques............................................................................. — 4 3.1 Logique du premier ordre........................................................................... — 4 3.2 Théorie des ensembles ............................................................................... — 5 3.3 Notions sur les systèmes de types............................................................. — 5 4. Méthodes ensemblistes.......................................................................... — 5 4.1 Méthode VDM.............................................................................................. — 5 4.2 Méthode Z .................................................................................................... — 6 4.3 Méthode B.................................................................................................... — 6 5. Types abstraits algébriques .................................................................. — 6 6. Domaine des protocoles ........................................................................ — 7 6.1 Estelle ........................................................................................................... — 7 6.2 Logique temporelle ..................................................................................... — 8 6.3 Approche synchrone ................................................................................... — 9 7. Logiques d’ordre supérieur, logiques constructives...................... — 9 7.1 Ordre supérieur............................................................................................ — 9 7.2 Introduction du typage................................................................................ — 9 7.3 Modes d’utilisation des logiques typées ................................................... — 10 8. Conclusion ................................................................................................. — 11 Pour en savoir plus........................................................................................... Doc. H 2 550 A DÉVELOPPEMENT ET VALIDATION DE LOGICIELS. MÉTHODES FORMELLES ________________________________________________________________________ Toute reproduction sans autorisation du Centre français d’exploitation du droit de copie est strictement interdite. H 2 550 − 2 © Techniques de l’Ingénieur, traité Informatique les spéciﬁcations. Ces raisons peuvent être aussi la non-conformité de l’appli- cation par rapport aux spéciﬁcations ou bien encore de simples problèmes de fonctionnement de l’application. La spéciﬁcation en langage dit naturel permet au spéciﬁcateur d’utiliser les moyens qui lui semblent les plus appropriés à ce qu’il veut décrire : le français ou l’anglais, un exemple de comportement, une table, un programme, une réfé- rence, etc. Ces moyens sont, de plus, accessibles au plus grand nombre d’infor- maticiens. En revanche, ils peuvent favoriser l’apparition d’ambiguïtés dissimulées dans un verbiage excessif ou peu structuré. Ils ne permettent aucune analyse sérieuse de détection des incohérences ou des incomplétudes dans les spéciﬁcations. Ils ne permettent ni d’obtenir une application certiﬁée conforme aux spéciﬁcations, ni de vériﬁer a posteriori qu’une application est conforme à ces mêmes spéciﬁcations. Les techniques formelles et leurs langages favorisent la maîtrise du cycle de vie du logiciel : — ils permettent une expression formelle des spécifications se prêtant à une interprétation précise, mathématique ; — ils permettent une analyse qualitative (vérification de cohérence) et quantitative (vérification de complétude) des spécifications ; — ils permettent, dans certains cas, la production semi-automatique de programmes certifiés conformes aux spécifications ; — ils permettent aussi la preuve a posteriori que l’application est bien conforme aux spécifications. Spéciﬁer formellement oblige en pratique à fouiller beaucoup plus profondément que ne le permettent les raisonnements ordinaires. L’expérience montre que la connaissance retirée d’un problème permet d’aborder le processus de réalisation avec beaucoup plus de conﬁance, car les descriptions sont très rigoureuses. Même dans un cadre où l’application produite ne sera pas confrontée formellement avec les spéciﬁcations originales, l’apport est fondamental. Il reste que la vériﬁcation formelle de la conformité d’une application à ses spéciﬁcations est parfois possible et ﬁgure l’élément concluant et fondamental des techniques formelles. Les techniques formelles de développement de logiciel ont beaucoup progressé au cours de la décennie écoulée. Il est devenu possible de traiter certaines applications réelles de manière entièrement formelle. Cependant, le discours de ses promoteurs s’est assagi, tant sur la taille des applications que l’on peut prétendre traiter que sur le degré de conﬁance que l’on peut obtenir. Ces techniques sont donc appliquées spéciﬁquement à certaines applications qui n’ont aucun droit à l’erreur, telles que des logiciels de pilotage d’engins. Elles sont également utilisables, théoriquement, dans un cadre plus général pour mini- miser le prix de revient d’une application en augmentant la ﬁabilité et en dimi- nuant les coûts de maintenance et d’évolution de celle-ci. 1. Généralités 1.1 Bref historique L’une des premières tentatives de rationalisation de la program- mation fut l’introduction d’assertions dans le corps des programmes impératifs représentés par des organigrammes [11]. Ces assertions sont des formules logiques décrivant un état des éléments du pro- gramme. On distingue les préconditions qui doivent être vériﬁées avant l’appel du programme, les post-conditions qui seront vériﬁées après l’exécution de celui-ci et les invariants de boucle qui traduisent la rémanence d’une propriété pendant l’exécution d’une structure itérative. L’utilisation des assertions et des règles du système permet de démontrer formellement des propriétés du programme. Cette méthode fut partiellement automatisée pour des programmes de type ALGOL. La méthode fut étendue et généralisée jusqu’à inclure des éléments de programme dans les assertions [17]. Dans le système de Hoare, les propriétés des programmes sont exprimées par des triplets {P } S {Q} où S est un programme, P sa précondition et Q sa post-condition. On dispose de règles de la forme : signiﬁant intuitivement que si S établit Q à partir de la précondition P et B, alors while B do S établit P et non B à partir de la précondition P. De telles règles sont utilisées pour démontrer la véracité des asser- tions ﬁgurant dans le programme. Elles furent même proposées [4] comme outil de déﬁnition de la sémantique d’un langage. La méthode de Hoare et ses descendants, par exemple la méthode des plus faibles conditions de Dijkstra [8], furent très longtemps les seuls outils permettant de prouver formellement, à la main ou de manière semi-automatique [15] [19] [29], les propriétés d’un programme. Il P B ∧ { }S Q { } P { } while B do S P B ¬ ∧ { } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ________________________________________________________________________ DÉVELOPPEMENT ET VALIDATION DE LOGICIELS. MÉTHODES FORMELLES Toute reproduction sans autorisation du Centre français d’exploitation du droit de copie est strictement interdite. © Techniques de l’Ingénieur, traité Informatique H 2 550 − 3 est à remarquer que des langages récents comme EIFFEL [21] mais aussi C et C++ proposent d’inclure explicitement les assertions dans la syntaxe. Une approche différente et plus ancienne trouve ses fondements dans LISP et les travaux de McCarthy [20] sur la programmation fonc- tionnelle. Dans ce style de programmation représenté par LISP ou d’autres langages plus rigoureux comme ML [22] [33], le programme est un objet mathématique qui apparaît comme sa propre spéciﬁ- cation et est directement sujet à une étude formelle sans l’intro- duction d’un formalisme supplémentaire. On retrouve ces caractéristiques dans les systèmes de programmation en logique [3] [5] où les formules logiques tiennent lieu de programmes. Ces langages, sous leur forme pure, sont dits déclaratifs. En pratique, cet idéal doit faire face à des compromis pour des raisons d’efﬁcacité ou lorsqu’il est nécessaire d’exprimer certains concepts, par exemple pour prendre en compte les changements subits par l’environne- ment dans lequel est plongé le programme considéré. Ces langages sont généralement réservés au maquettage d’applications ou au traitement de problèmes spéciﬁques nécessitant souplesse et dynamicité. Les techniques ensemblistes sont représentées principalement par Z [32], B [1] et VDM [18]. Elles occupent une place de choix, car elles sont actuellement utilisées par l’industrie informatique et nous y reviendrons de manière plus détaillée (§ 4). Nous qualiﬁons ces techniques d’ensemblistes, car les spéciﬁcations y sont énoncées au moyen de notations provenant de la théorie des ensembles et leurs fondements appartiennent à la tradition logique de la théorie axio- matique des ensembles. Des outils de preuves et de rafﬁnage semi- automatique, intégrés dans des ateliers de génie logiciel (AGL), visent à permettre l’écriture de programmes certiﬁés corrects par rapport aux spéciﬁcations. Les techniques de spéciﬁcation algébrique [12] s’appuient sur la notion de type abstrait algébrique. Nous y reviendrons également (§ 5). Des développements récents ont abouti à des langages et des environnements proposant assistance au moyen d’outils d’édition, de modularisation et de preuves semi-automatiques. Nous verrons uploads/Philosophie/ developpemen-et-validation-de-logiciels-methodes-formelles-pdf.pdf