Méthode formelle (informatique) - Définition

Vérification

Une spécification peut être utilisée comme base pour prouver des propriétés sur le système. La spécification est le plus souvent une représentation abstraite (avec moins de détails) du système en développement: débarrassé de détails encombrants, il est en général plus simple de prouver des propriétés sur la spécification que directement sur la description complète et concrète du système.

Certaines méthodes, comme la Méthode B, s'appuient sur ce principe: le système est modélisé à plusieurs niveaux d'abstraction, en partant du plus abstrait et en allant au plus concret (ce processus est appelé « raffinement » puisqu'il ajoute des détails au fur et à mesure); la méthodologie assure que toutes les propriétés prouvées sur les modèles abstraits sont conservées sur les modèles concrets. Cette garantie est apportée par un ensemble de preuves dites «de raffinement».

Principaux outils

• ACL2 : démonstration de théorèmes automatisée.
• AtelierB : spécification et preuve avec la méthode B.
• CADP : construction et analyse de processus distribués
• Coq : assistant d'aide à la preuve (c'est-à-dire formalisation de preuves et démonstration semi-automatisée).
• Murφ : démonstration de propriétés.
• Prototype Verification System : assistant d'aide à la preuve.
• SMV, nuSMV : démonstration de propriétés avec BDDs et SAT.
• zChaff : démonstration avec SAT.

Méthodes formelles ou semi-formelles

• Approche basée sur des états
  • Z voir Notation Z
  • SAZ
  • Méthode B classique voir Méthode B
  • ASM
  • TLA+

• Approche basée sur des événements
  • Action Systems
  • Méthode B événementielle voir Méthode B
  • VHDL
  • Esterel
  • SDL
  • LOTOS
  • E-LOTOS
  • EB3

• Algébriques :
  • Larch :Larch family
  • CASL : Common Algebraic Specification Language

• Autre approche
  • Coq (logiciel)
  • Réseau de Petri
  • Algèbre de processus