Introduction aux méthodes formelles

Jour 1

Définition des méthodes formelles

Approche par les caractéristiques des méthodes formelles en s’appuyant sur un exemple introductif.

Historique des méthodes formelles

• Apparition du besoin (bugs catastrophiques) et domaines relatifs
• Liens avec la maîtrise de la complexité logicielle
• Liens avec la maîtrise de l’effort de test

Concepts communs aux méthodes formelles

• Sémantique: ce que fait un logiciel/un système, exprimer ce qu’on veut qu’il fasse
• Abstraction: maîtrise des spécifications et des exigences
• Modularité: maîtrise de la complexité
• Raffinement: maîtrise du développement
• Vérification: respect des spécifications et des exigences

Exemples de mise en œuvre

Présentation de différentes méthodes formelles et des outils et techniques associés:

• Méthodes basées sur la preuve
• Model-checking
• Analyse statique par interprétation abstraite

Jour 2

Techniques de preuve formelle

• Fonctionnalités (détection de contre-exemples, recherche de contradiction, vérification de propriétés, etc)
• Mécaniques de preuve
• Conditions de mise en œuvre (hypothèses d’environnement, liens formalisme<->langage de preuve, formalisation des objectifs de preuve)
• Outillage

Types de techniques

• Règles d’inférence et tactiques
• Preuve par induction
• Vérification de modèle (model-checking)

Besoins

• Réécriture
• Vérification de propriétés et preuve sur le code source

Problématiques

• Preuve automatique, preuve interactive, importance du rejeu de preuve
• Divergence
• Validité de la preuve
• Besoins sur les hypothèses: existence d’hypothèses sur l’environnement du système considéré, difficultés sur la validité des hypothèses

Exemples de mise en œuvre

Les notions abordées seront illustrées sur des exemples de mise en œuvre d’outils de preuve, type AtelierB, Simulink Design Verifier, Coq, etc

Aucune expérience n’est nécessaire, cependant les publics ayant une formation initiale orientée ingénierie, mathématiques ou informatique se sentiront plus à l’aise.

En distanciel:

• Un accès internet stable avec un débit correct permettant le partage d’affichage à distance
• Un PC/Mac avec l’outil Teams ainsi qu’un accès non restreint à Internet

Cette formation vise toute personne travaillant dans le milieu des systèmes embarqués critiques basés sur du logiciel, et sur lesquels de fortes exigences pèsent quant aux garanties de sûreté de fonctionnement. Elle s’adresse donc notamment:

• Aux concepteurs qui se demandent quel serait l’impact de l’utilisation des méthodes formelles sur leurs systèmes
• Aux décideurs se posant la question du rapport effort/bénéfice de l’utilisation des méthodes formelles
• Aux développeurs logiciels qui souhaitent comprendre comment l’utilisation des méthodes formelles s’articule par rapport aux programmes qu’ils conçoivent

Expert en méthodes formelles

Présentation PowerPoint projetée

Évaluation en début et fin de formation

5 jours ouvrés avant le début de la formation (si financement OPCO).

Une attestation de formation conforme aux dispositions de l’Article L6353-1 alinéa 2 remise au stagiaire.