Soutenance mémoire
Approches générales
Les méthodes formelles sont des techniques, basées sur les mathématiques, pouvant être utilisées à toutes les étapes du développement logiciel. Par formelles, on désigne des méthodes dont le but principal est de rendre précises des idées de développement auparavant vagues ou simplement intuitives [1]. Contrairement à d’autres méthodes de design,les méthodes formelles se basent sur les preuves mathématiques pour assurer un comportement correct. A la mesure où les systèmes deviennent de plus en plus complexes, et la sécurité une question de plus en plus importante, les approches formelles offrent un autre niveau d’assurance. Les méthodes formelles diffèrent d’autres systèmes de conception par l’utilisation d’une vérification formelle, c’est-à-dire que les principes de base du système doivent être correctement prouvés avant qu’ils soient admis. Les méthodes de conception traditionnelles utilisent des tests intensifs pour vérifier le comportement des systèmes, mais les tests ne peuvent aboutir qu’à des conclusions limitées. Notons en effet que les tests révèlent seulement où le système n’échouera pas, mais ils ne peuvent décrire en aucun cas le comportement du système en dehors du scénario d’essai. En revanche, du point de vue formel, une fois qu’un théorème est prouvé être vrai, il reste vrai. Toutefois, il est à souligner que la vérification formelle n’obvie pas au besoin d’essai. Dans plusieurs cas,des ingénieurs ont rapportés des défauts dans leur système une fois après ils passaient en revue, d’une manière formelle, leurs conceptions. D’une façon générale, une conception basée sur les méthodes formelles peut être subdivisée en trois étapes :
1. Spécification formelle : Phase durant laquelle on définit rigoureusement un système en utilisant un langage de modélisation. Ce dernier permet de modéliser une structure complexe à partir de règles et de types prédéfinis. Cette phase consiste à convertir les spécifications informelles en notation algébrique.
2. Vérification : Comme souligné ci-dessus, les méthodes formelles diffèrent des autres systèmes de spécification de par leur emphase sur les preuves et l’exactitude. Un ingénieur spécifiant un système par les méthodes formelles développe en fait un ensemble de théorème concernant son système. En prouvant que ces théorèmes sont corrects, il démontre que son système est exempt de défaut. La phase de vérification est un processus long et difficile. Même les plus simples des systèmes disposent en effet de plusieurs théorèmes, dont chacun doit être prouvé. Vu aussi que même les plus basiques des preuves mathématiques sont quelquefois complexes, les systèmes formels utilisent des outils automatisés comme moyen d’assistance à la démonstration preuves.
3. Implémentation : Une fois qu’un modèle est spécifié et prouvé, il est alors mise en oeuvre. La spécification précédemment définie est converti code.Il faut savoir en effet que la rigueur mathématique peut être utilisée à tous les stades du cycle de développement : analyse des besoins, spécification, conception architecturale, conception détaillée, implémentation, test et maintenance.La première étape essentielle dans un processus de développement d’application de haute qualité est l’analyse des besoins. Les méthodes formelles peuvent êtres utiles si on veut rendre l’expression des besoins explicite, claire et précise. Les outils dont ces méthodes disposent peuvent être utilisés pour la vérification de la complétude, de la traçabilité, de la vérifiabilité et de la réutilisabilité des documents d’analyse (de besoin). Comme déjà introduit ci-dessus, les méthodes formelles sont utilisées pour la spécification logiciel, en élaborant des comportements précis non ambigus tout en évitant les détails et contraintes sur la façon suivant laquelle le logiciel doit être implémenté. ASM (Abstract States Machine), VDM (Vienna Development Methods), la méthode B et la notation Z en constituent des exemples concrets. Les systèmes complexes requièrent une organisation soigneuse de leur structure architecturale. Un modèle du système, supprimant tous détails d’implémentation, permet à l’architecte développeur de se concentrer sur les analyses et décisions les plus cruciales concernant la structure du système. Le but reste évidemment de pouvoir toujours mieux répondre aux exigences imposées. WRIGHT est un exemple de langage de description architecturale utilisable dans ce domaine. Il est basé sur la formalisation du comportement abstrait des composants architecturaux et de leurs connecteurs. Les méthodes formelles se retrouvent aussi à l’étape de conception par l’utilisation des techniques de raffinement. Plusieurs auteurs et chercheurs ont mis en évidence le rôle central de ce genre de techniques : Hoare C. en 1972, Jones C. B. en 1990 en introduisant VDM, Dijkstra E. W. en 1975 et MORGAN C. en 1988 pour aboutir aux principes des calculs de raffinement.
Domaine aéronautique
Le domaine du transport aérien a été l’un des premiers à mettre en place un référentiel normatif qui couvre l’ensemble de la réalisation d’un système. Ce référentiel prend en compte les aspects sûreté de fonctionnement. Tout avion fait l’objet d’une certification. Cette certification vise a démontrer que le système est conforme à la réglementation en vigueur. Cette réglementation impose le respect d’un référentiel. Ce référentiel est actuellement composé :
• Pour les applications de type avion : de la norme DO-178, intitulé « Software considerations in airborne systems and equipement certification », pour les aspects développement logiciel, d’un référentiel métier constitué d’un ensemble de règlements FAR3/JAR4 qui sont applicables à tous les avionneurs et d’un ensemble de guides méthodologiques produits par la communauté aéronautique
• Pour les applications au sol : de la norme DO-278 (« Guidelines for communication, navigation, surveillance, and Air traffic management (CNS/ATM) Systems software integrity assurance ») La norme DO-178 a été révisée en 2009. Cette révision vise à introduire : les méthodes formelles, les nouvelles techniques de vérification du logiciel tel l’interprétation abstraite de programme et les aspects orienté objet. Le JAA (Joint Aviation Authorities), organisme regroupant les autorités réglementaires d’un certain nombre de pays, étudie et rédige des règles communes, dites codes JAR (Joint Aviation Requirement), dans les domaines de la sécurité et de l’exploitation des aéronefs. Chaque pays adhérent au JAA s’engage à introduire les JAR dans sa propre réglementation (ce qui leur donne force de loi) avec les seules adaptations nécessaires au respect de son droit national. Ce référentiel a été récemment complété par la norme DO-254 (« Electronique hardware – design assurance guidance for airborne electronic hardware ») qui s’applique aux aspects composants numériques tels que les FPGA et autres ASIC. Cette famille de composants remplace une partie logicielle et matérielle par un circuit intégré. La problématique engendrée est liée au fait qu’il est difficile de vérifier et de valider le comportement de ces circuits et que de part leurs natures (logiciel et matériel), il est difficile de démontrer l’absence de faute de conception.
Taxonomie et morphologie des schémas
Les schémas courants sont habituellement de deux sortes :
Orientés données : ils regroupent ou décrivent alors un ensemble de données. Ils donnent possiblement leur état initial.
Orientés opérations : ils donnent alors des manipulations abstraites des données définies ailleurs, possiblement dans des schémas orientés données.Le langage Z permet ainsi de décrire, à un niveau très abstrait (c’est-à-dire fortement découplé de toute implémentation logicielle), un produit logiciel sous une perspective formelle alignée sur l’information que celui-ci traite. En Z, tout s’articule en effet autours des données : le langage décrit formellement celles-ci, et la façon dont elles sont manipulées. Un schéma est toujours composé de trois parties :
• Un nom qui identifie le schéma et ayant une portée globale sur la spécification.
• Une partie déclarative (pouvant être vide) qui définit les différentes données membres du schéma. Les données définies pour la première fois sont de portée locale. Son contenu est appelée signature.
• Une partie prédicative (pouvant être vide) qui énumère les contraintes que doivent respecter les données accessibles dans la portée courante, localement ou globalement. Dans le cas de schémas « orientés opérations », la partie prédicative se termine habituellement par des expressions qui ne sont pas des prédicats, mais plutôt des affectations de certaines données membres (utilisant le symbole =). Par le cadre formel, il est à noter que chaque donnée ne pourra subir qu’une seule affectation dans un même schéma ; ces affectations permettent de décrire les différentes opérations abstraites effectuée par ces schémas.
Preuves automatiques du modèle en utilisant Z/EVES
Ce chapitre présente le système Z/EVES. Il s’agit d’un système dédié à l’analyse des spécifications Z. Il est généralement utilisé pour l’analyse syntaxique, la vérification du typage et de l’application des fonctions dans leur domaine, mais aussi pour l’expansion des schéma, pour le calcul de préconditions, pour la réalisation d’un raffinement et pour prouver différentes propriétés. Le langage à utiliser pour les interactions avec Z/EVES est dénommé Z/LATEX. Z/EVES est basé sur le système EVES et utilise le prouveur de théorème de celui-ci pour faire chacune des étapes de ses preuves. Cependant, il n’est pas nécessaire de connaître EVES ou son langage (Verdi) pour utiliser Z/EVES. L’interface Z de EVES a été développé par Irwin Meisels conjointement avec le Département de la Défense des Etats-Unis. Et EVES lui-même a été développé par plusieurs auteurs dont Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, et ceci sous l’égide du Département de la Défense Nationale du Canada. Ce démonstrateur dispose d’une base de connaissances en théorie des ensembles et en logique du premier ordre. Les règles d’inférence qu’il utilise sont reliées à ces deux domaines. En effet, plusieurs théorèmes peuvent être utiles pour faire de la démonstration de propriétés. Parmi ces théorèmes, on retrouve autant des propriétés utiles que des règles d’inférence. Ce chapitre donne un bref aperçu de l’utilité de Z/EVES dans la démarche de validation du modèle proposé dans ce mémoire. Il inclut notamment les usages les plus courants de Z/EVES à l’aide d’exemples tirés de ce modèle. Dans ce qui suit, Z/EVES sera utilisé principalement :
• pour faire l’expansion d’un schéma,
• pour vérifier la syntaxe et la cohérence des types,
• pour vérifier l’application des fonctions dans leur domaine,
• pour vérifier les conditions initiales de chaque opération.
|
Table des matières
Remerciements
Résumé
Listes diverses
Introduction
1 Aperçu sur les applications des méthodes formelles
1.1 Approches générales
1.2 Historique
1.3 Référentiel normatif
1.3.1 Domaine aéronautique
1.3.2 Domaine spatial
1.3.3 Domaine ferroviaire
1.3.4 Domaine automobile
1.3.5 Domaine nucléaire
1.4 Utilisation actuelle et tendance
1.4.1 Analyse des données
1.4.2 Résultats
2 Notions de base du langage Z
2.1 Logique propositionnelle et logique des prédicats
2.1.1 Logique propositionnelle
2.1.2 Logique des prédicats
2.2 Théorie des ensembles
2.2.1 Rappel
2.2.2 Extension Z de la théorie des ensembles
2.3 Relations
2.3.1 Notions générales
2.3.2 Fonctions
2.4 Schémas
2.4.1 Taxonomie et morphologie des schémas
2.4.2 Notation des schémas
2.4.3 Interaction des schémas
2.4.4 Aide à la présentation
2.4.5 Schémas génériques
2.5 Object-Z
3 Modélisation formelle du noyau
3.1 Introduction
3.2 Types primaires
3.2.1 Processus
3.2.2 Registres
3.2.3 Interruption
3.3 Abstractions nécessaires
3.4 Gestion des priorités
3.5 Processus courant et processus prêts
3.6 Messages et sémaphores
4 Preuves automatiques du modèle en utilisant Z/EVES
4.1 Introduction
4.2 Expansion d’un schéma
4.3 Vérification de la syntaxe et de la cohérence des types
4.4 Analyse de l’application des fonctions dans leur domaine
4.5 Vérification des conditions initiales
4.6 Théorème des préconditions
Conclusion
Annexes
Annexe 1
Annexe 2
Télécharger le rapport complet
