Worldlex Wiki En informatique , les méthodes formelles sont des techniques mathématiquement rigoureuses permettant de spécifier , développer, analyser et vérifier les systèmes logiciels et matériels . L'utilisation de méthodes formelles pour la conception de logiciels et de matériels repose sur l'idée que, comme dans d'autres disciplines de l'ingénierie, une analyse mathématique appropriée peut contribuer à la fiabilité et à la robustesse d'une conception.
Les méthodes formelles utilisent divers éléments fondamentaux de l'informatique théorique , notamment les calculs logiques , les langages formels , la théorie des automates , la théorie du contrôle , la sémantique des programmes , les systèmes de types et la théorie des types .
processus de développement .Spécification
Synthèse
Une fois qu'une spécification formelle a été élaborée, celle-ci peut servir de base pour prouver les propriétés de la spécification et, par déduction, les propriétés de l'implémentation du système.
Vérification de la signature
La vérification par signature consiste à utiliser un outil de vérification formel hautement fiable. Un tel outil peut remplacer les méthodes de vérification traditionnelles (il peut même être certifié).
Preuve dirigée par l'humain
Parfois, la motivation pour prouver la correction d'un système n'est pas le besoin évident de s'assurer de sa correction, mais le désir de mieux le comprendre. Par conséquent, certaines preuves de correction sont rédigées à la manière des démonstrations mathématiques : manuscrites (ou composées), en langage naturel , avec le niveau d'informalité propre à ce type de démonstrations. Une « bonne » démonstration est une démonstration lisible et compréhensible par d'autres personnes.
Les détracteurs de ces approches soulignent que l' ambiguïté inhérente au langage naturel permet aux erreurs de passer inaperçues dans ces démonstrations ; souvent, des erreurs subtiles peuvent se cacher dans les détails de bas niveau généralement négligés par ces démonstrations. De plus, l'élaboration d'une telle démonstration de qualité exige un haut niveau de compétences et de maîtrise mathématiques.
Preuve automatisée
En revanche, on observe un intérêt croissant pour la production de preuves automatisées de la correction de tels systèmes. Les techniques automatisées se répartissent en trois grandes catégories :
- Démonstration automatique de théorèmes , dans laquelle un système tente de produire une preuve formelle à partir de zéro, étant donné une description du système, un ensemble d' axiomes logiques et un ensemble de règles d'inférence .
- La vérification de modèles consiste à vérifier certaines propriétés d'un système en effectuant une recherche exhaustive de tous les états possibles que le système pourrait atteindre lors de son exécution.
- Interprétation abstraite , dans laquelle un système vérifie une sur-approximation d'une propriété comportementale du programme, en utilisant un calcul de point fixe sur un réseau (éventuellement complet) le représentant.
Certains démonstrateurs de théorèmes automatiques nécessitent des indications sur les propriétés « intéressantes » à étudier, tandis que d'autres fonctionnent sans intervention humaine. Les vérificateurs de modèles peuvent rapidement se retrouver submergés par la vérification de millions d'états sans intérêt s'ils ne disposent pas d'un modèle suffisamment abstrait.
Les partisans de ces systèmes affirment que leurs résultats présentent une plus grande certitude mathématique que les démonstrations réalisées manuellement, puisque tous les détails fastidieux sont vérifiés algorithmiquement. La formation requise pour utiliser ces systèmes est également moindre que celle nécessaire pour produire manuellement de bonnes démonstrations mathématiques, ce qui rend ces techniques accessibles à un plus grand nombre de praticiens.
Les critiques soulignent que certains de ces systèmes s'apparentent à des oracles : ils énoncent une vérité sans l'expliquer. Se pose également le problème de la « vérification du vérificateur » ; si le programme qui contribue à la vérification n'est pas lui-même éprouvé, la validité des résultats obtenus peut être mise en doute. Certains outils modernes de vérification de modèles produisent un « journal de preuve » détaillant chaque étape de leur démonstration, permettant ainsi, avec les outils appropriés, une vérification indépendante.
L'atout majeur de l'approche par interprétation abstraite réside dans sa capacité à fournir une analyse fiable, c'est-à-dire sans faux négatifs. De plus, elle est facilement extensible, grâce à l'ajustement du domaine abstrait représentant la propriété à analyser et à l'application d'opérateurs d'élargissement pour une convergence rapide.
Techniques
solveurs SAT
Applications
Les méthodes formelles sont appliquées dans différents domaines du matériel et du logiciel, notamment les routeurs , les commutateurs Ethernet , les protocoles de routage , les applications de sécurité et les micro-noyaux de systèmes d'exploitation tels que seL4 . Plusieurs exemples montrent leur utilisation pour vérifier la fonctionnalité du matériel et des logiciels utilisés dans les centres de données . IBM a utilisé ACL2 , un démonstrateur de théorèmes, lors du développement du processeur AMD x86. Intel utilise ces méthodes pour vérifier son matériel et son firmware (logiciel permanent programmé dans une mémoire morte ) . Dansk Datamatik Center a utilisé des méthodes formelles dans les années 1980 pour développer un système de compilation pour le langage de programmation Ada , qui est devenu par la suite un produit commercial à succès.
Plusieurs autres projets de la NASA appliquent des méthodes formelles, comme le Next Generation Air Transportation System , l'intégration des systèmes d'aéronefs sans pilote dans le système national de l'espace aérien et le système aéroporté de résolution et de détection coordonnées des conflits (ACCoRD) . La méthode B avec Atelier B [ est utilisée pour développer des automatismes de sécurité pour les différents métros installés dans le monde par Alstom et Siemens , ainsi que pour la certification selon les Critères communs le développement de modèles de systèmes par ATMEL et STMicroelectronics .
La vérification formelle est fréquemment utilisée dans le domaine du matériel par la plupart des grands fabricants, tels qu'IBM, Intel et AMD. Intel a eu recours à des méthodes formelles pour vérifier le fonctionnement de ses produits dans de nombreux domaines, notamment la vérification paramétrée d'un protocole à cohérence de cache , la validation du moteur d'exécution du processeur Intel Core i7 (par démonstration de théorèmes, diagrammes de décision binaire et évaluation symbolique), l'optimisation de l'architecture Intel IA-64 à l'aide du démonstrateur de théorèmes HOL Light et la vérification d' un contrôleur Ethernet Gigabit double port haute performance compatible avec le protocole PCI Express et la technologie de gestion avancée Intel (AMT) à l'aide de Cadence . De même, IBM a utilisé des méthodes formelles pour la vérification des portes logiques , des registres et la vérification fonctionnelle du microprocesseur IBM Power7
Dans le développement logiciel
En développement logiciel , les méthodes formelles sont des approches mathématiques permettant de résoudre les problèmes logiciels (et matériels) aux niveaux des exigences, des spécifications et de la conception. Elles sont généralement appliquées aux logiciels et systèmes critiques pour la sécurité, tels que les logiciels avioniques . Les normes d'assurance de la sécurité logicielle, comme la norme DO-178C, autorisent l'utilisation de méthodes formelles par le biais de compléments, et les Critères communs les imposent aux niveaux de catégorisation les plus élevés.
Pour les logiciels séquentiels, les exemples de méthodes formelles incluent la méthode B , les langages de spécification utilisés dans la démonstration automatique de théorèmes , RAISE et la notation Z.
En programmation fonctionnelle , les tests basés sur les propriétés ont permis la spécification mathématique et le test (voire le test exhaustif) du comportement attendu des fonctions individuelles.
Le langage de contraintes d'objets (et ses spécialisations telles que le langage de modélisation Java ) a permis de spécifier formellement les systèmes orientés objet, même s'ils ne sont pas nécessairement vérifiés formellement.
Pour les logiciels et systèmes concurrents, les réseaux de Petri , l'algèbre des processus et les machines à états finis (qui sont basées sur la théorie des automates ; voir aussi machine à états finis virtuelle ou machine à états finis pilotée par événements ) permettent la spécification de logiciels exécutables et peuvent être utilisés pour construire et valider le comportement de l'application.
Une autre approche des méthodes formelles en développement logiciel consiste à rédiger une spécification sous une forme logique – généralement une variante de la logique du premier ordre – puis à exécuter directement cette logique comme s'il s'agissait d'un programme. Le langage OWL , basé sur la logique de description , en est un exemple. Des travaux portent également sur la conversion automatique d'une version de l'anglais (ou d'une autre langue naturelle) vers et depuis la logique, ainsi que sur l'exécution directe de cette dernière. On peut citer comme exemples Attempto Controlled English et Internet Business Logic, qui ne cherchent pas à contrôler le vocabulaire ni la syntaxe. Les systèmes prenant en charge la conversion bidirectionnelle anglais-logique et l'exécution directe de cette dernière ont la particularité de pouvoir expliquer leurs résultats en anglais, à un niveau métier ou scientifique.les générateurs de cas de test .
Certains praticiens estiment que la communauté des méthodes formelles a survalorisé la formalisation complète d'une spécification ou d'une conception. Ils soutiennent que l' expressivité des langages utilisés, ainsi que la complexité des systèmes modélisés, rendent la formalisation complète difficile et coûteuse. En alternative, diverses méthodes formelles légères , privilégiant la spécification partielle et une application ciblée, ont été proposées. Parmi ces approches légères, on peut citer la notation de modélisation objet Alloy , la synthèse par Denney de certains aspects de la notation Z avec le développement piloté par les cas d'utilisation , et les outils CSK VDM .
Méthodes et notations formelles
Il existe diverses méthodes et notations formelles.
Langues de spécification
- Machines à états abstraits (ASM)
- Une logique computationnelle pour Applicative Common Lisp (ACL2)
- mannequin acteur
- Alliage
- Langage de spécification ANSI/ISO C (ACSL)
- Langage de spécification du système autonome (ASSL)
- Méthode B
- CADP
- Langage de spécification algébrique commun (CASL)
- Esterel
- Langage de modélisation Java (JML)
- Assistant logiciel basé sur les connaissances (KBSA)
- Lustre
- mCRL2
- Développeur parfait
- Réseaux de Petri
- Programmation prédictive
- Calculs de processus
- AUGMENTER
- Langage de modélisation Rebeca
- SPARK Ada
- Langage de spécification et de description
- TLA+
- USL
- VDM
- VDM-SL
- VDM++
- Notation Z
Vérificateurs de modèles
Solveurs et compétitions
De nombreux problèmes de méthodes formelles sont NP-difficiles , mais peuvent être résolus dans des cas pratiques. Par exemple, le problème de satisfaisabilité booléenne est NP-complet d'après le théorème de Cook-Levin , mais les solveurs SAT peuvent résoudre une grande variété d'instances de grande taille. Il existe des « solveurs » pour divers problèmes rencontrés en méthodes formelles, et de nombreuses compétitions périodiques permettent d'évaluer les performances de pointe dans la résolution de ces problèmes.
- Le concours SAT est une compétition annuelle qui compare les solveurs SAT. Les solveurs SAT sont utilisés dans des outils de méthodes formelles tels que Alloy .
- CASC est un concours annuel de démonstrateurs de théorèmes automatisés .
- SMT-COMP est une compétition annuelle de solveurs SMT , qui sont appliqués à la vérification formelle .
- CHC-COMP est un concours annuel de solveurs de clauses de Horn contraintes , qui ont des applications en vérification formelle.
- QBFEVAL est une compétition biennale de solveurs pour les vraies formules booléennes quantifiées , qui ont des applications dans la vérification de modèles .
- SyGuS-COMP est un concours annuel d' outils de synthèse de programmes .