CONTENU DÉTAILLÉ
1. Introduction (3 heures)
1.1 Présentation générale des méthodes formelles; justification de leur utilisation, spécifications et vérification de logiciels.
1.2 Révision des concepts de base : ensembles, logique et propositions.
2. Langage de spécifications OCL (15 heures)
2.1 Modélisation : UML, MDA, OCL, la notion de contraintes.
2.2 Collections, bags, séquences, distinctions.
2.3 Vérification de modèles.
2.4 Études de cas : Génération de code et discussion.
3. Spécifications, analyse et vérification de systèmes concurrents (9 heures)
3.1 FSP et RdP : processus, exécution concurrente, objets partagés et exclusion mutuelle.
3.2 FSP et RdP : propriétés de vivacité et de sécurité, analyses, raisonnement.
3.3 Invariants de transitions et de places
4. Spécifications, analyse et vérification de systèmes concurrents (9 heures)
4.1 Processus, exécution concurrente, objets partagés et exclusion mutuelle, blocages, formalismes.
4.2 Moniteurs et synchronisation de conditions, blocages et vivacité.
4.3 Logique CTL
5. Application, approches et limites (3 heures)
5.1 UML exécutable.
5.2 Autres approches
5.3 Limites et contraintes.
5.3 Vérification de modèles vs technique de preuve.