À la fin du cours, l'étudiant(e) aura assimilé les notions suivantes :

• Niveaux d’abstraction et formalisation

• Différence entre langage formel et semi-formel

• Vérification de modèles

• Avantages et limites des méthodes formelles

• Langage de spécification OCL pour UML

• Spécification avec des diagrammes états/transitions

• Spécifications de systèmes concurrents

• Spécifications de systèmes temps réel

À la fin du cours, l’étudiant(e) sera capable de :

• Lire des spécifications formelles écrites dans un langage proche de la logique du premier ordre;

• Écrire des spécifications formelles dans un langage proche de la logique du premier ordre;

• Comprendre des spécifications formelles écrites par des professionnels;

• Spécifier un modèle UML avec OCL;

• Spécifier un modèle simple d’un système concurrent;

• Vérifier avec l’aide d’outils ses modèles UML/OCL;

• Analyser les résultats de ses vérifications.

• 3.5 heures de cours et 2 heures de laboratoire par semaine. Certains documents pertinents au cours (mémos, exercices, solutionnaires, énoncés de travaux, fichiers d'exemples, etc.) seront placés régulièrement sur le site WEB du cours. Il est de la responsabilité de l'étudiant de consulter régulièrement ce site.

• Les laboratoires visent l'assimilation des notions vues au cours et la mise au point des travaux pratiques.

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.

• UML/OCL: USE (Université de Bremen)
• Automates temporisés/CTL: UPPAAL
• Réseaux de Petri: à déterminer

À noter qu’une moyenne inférieure à 50% dans les évaluations individuelles entraine automatiquement un échec au cours.

• Examen intra.............................35 %
• Examen final...........................................................35 %
• Trois (3) laboratoires (10 %, 10 %, 10 %) en équipe ..................30 %

• 1er jour après la date prévue de la remise: -20%
• 2ème jour après la date prévue de la remise: -50%
• Jours suivants: la note zéro est attribuée

Aucun

BENETT, Simon, SKELTON, John et LUNN, Ken (2001), UML, McGraw-Hill.

JACKSON, Daniel (2002) Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, No 2, pp. 256-290.

JACKSON, D. (2006), Dependable Software by Design, Scientific American, June.

JACKSON, Daniel, JACKSON, Michael (2006) Separating Concerns in Requirements Analysis: An Example. M. Butler, C. Jones, A. Romanovsky, E. Troubitsyna (editors). Chapter of Rigorous development of complex fault tolerant systems. Springer-Verlag.

JACKSON, Daniel (2011) Software Abstraction, MIT Press.

WARMER, Jos, KLEPPE, Anneke (2003) The Object Constraint Language (2nd Edition) Getting your Models Ready for MDA, Addison-Wesley.

* Consultez le site WEB du cours pour des références complémentaires. Les références précédées d’un point, « • » sont fortement suggérées.

Consultez le site MOODLE du cours pour la liste complète et constamment mise à jour des outils pertinents.