Formation, conseil et accompagnement pour le développement professionnel des personnes, des équipes et des organisations

Principes, techniques et applications au développement de systèmes et logiciels complexes.
La vérification et la validation (V&V) représentent une part importante dans le développement des systèmes critiques, notamment à cause de la taille et la complexité croissantes de ces systèmes. Les techniques classiques de V&V que sont la simulation et le test ne garantissent pas l’exhaustivité de la vérification et sont encore très manuelles, donc très coûteuses.
Les méthodes formelles sont des techniques alternatives, fondées sur des bases mathématiques, permettant la spécification et le développement de systèmes, ainsi que la vérification automatique de propriétés. Un éventail de langages et de techniques formels existe pour traiter différents types de propriétés à différents niveaux de développement des systèmes.

1. Présenter les fondements mathématiques des méthodes formelles
2. Présenter les grandes catégories de techniques existantes (et les outils associés)
3. Montrer les applications concrètes de ces techniques à la modélisation et à la vérification de systèmes, d’architectures, de logiciels

 Introduction et présentation des techniques existantes

- Contexte, motivations, objectifs

- Concepts communs

- Techniques de vérification existantes : model checking, preuve, interprétation abstraite

Méthodes formelles pour l'analyse de la sûreté de fonctionnement des systèmes embarqués

- Description formelle des systèmes et des exigences de sûreté de fonctionnement.

- Techniques de vérification associées (génération automatique d'arbres et de séquences de défaillances).

Méthodes formelles pour l'évaluation des performances temporelles d'un système temps réel distribué

- Techniques formelles pour le calcul "worst case execution time"  (WCET) d'un programme informatique

- Méthode d'analyse d'ordonnançabilité pire cas en configuration mono-processeur, puis extension au multi-processeur

- Méthode d'analyse de latence de bout en bout pire cas pour les réseaux embarqués (réseau CAN et réseau commuté)

- Ouverture aux méthodes d'évaluation probabiliste de réseaux de file d'attente (à base de chaîne de Markov et de réseaux de Petri stochastiques).

Méthodes formelles pour la vérification de logiciels

- Panorama des techniques existantes

          *  Ingénierie dirigée par les modèles et méthodes formelles

          *  Vérification de programmes

- Application industrielle : vérifications formelles de logiciels avioniques

Méthode pédagogique
Présentation des fondamentaux, de l'état de l'art, des dernières avancées
Illustration par des exemples concrets issus de l'industrie