Logo ÉTS
Session
Cours
Responsable(s) Sylvie Ratté

Se connecter
 

École de technologie supérieure
Département de génie logiciel et des TI
Responsable(s) de cours : Sylvie Ratté


PLAN DE COURS

Été 2017
MGL848 : Validation et vérification de modèles en génie logiciel (3 crédits)



Préalables
Aucun préalable requis




Descriptif du cours
Ce cours vise à procurer à l'étudiant une connaissance approfondie des méthodes formelles et semi-formelles pour la description et l’analyse de matériels ou de produits logiciels. Il vise également à faire comprendre les avantages et les limites de ces méthodes.

À la fin du cours, l'étudiant sera en mesure de produire un modèle abstrait et formel d’un système, de l’utiliser pour démontrer certaines propriétés, de d'expliquer comment ces propriétés répondent aux spécifications essentielles/critiques du système.

L'étudiant devra également être capable de lire et comprendre des spécifications formelles écrites par des professionnels et de produire des spécifications formelles de systèmes de complexité moyenne. Il possèdera une très bonne connaissance des méthodes existantes et saura discuter intelligemment des avantages et des inconvénients de l’utilisation de telles approches.



Objectifs du cours
  • produire un modèle abstrait à partir d'une spécification de système rédidigée en langue naturelle;
  • valider et interpréter des modèles abstraits réalisés par ses pairs;
  • utiliser des outils pour valider et vérifer des modèles;
  • rédiger des contraintes et des propriétés en utilisant des langages formels ou semi-formels;
  • développer un esprit critique et une sensibilité accrue aux défauts des modèles.



Stratégies pédagogiques

Les 3.5 heures de cours sont interactifs et collaboratifs. Le matériel théorique est rendu disponible à l'avance. Les séances visent à approfondir les notions au travers des exercices pratiques et de courtes présentations magistrales.




Utilisation d’appareils électroniques

Il est fortement conseillé d'apporter son ordinateur ou de travailler en équipe avec un étudiant qui aura apporté le sien.




Horaire
Groupe Jour Heure Activité
01 Mardi 18:00 - 21:30 Activité de cours
Jeudi 18:00 - 21:30 Deuxième activité de cours



Coordonnées de l’enseignant
Groupe Nom Activité Courriel Local Disponibilité
01 Sylvie Ratté Activité de cours Sylvie.Ratte@etsmtl.ca A-4482



Cours

1.    Introduction (3 heures[1])

1.1    Présentation des méthodes formelles; 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, différence avec Z

2.3    OCL (suite) et sa transcription en code

2.4    Études de cas : Génération de code et discussion

3.    Automates, diagrammes états/transitions, diagrammes d’activités (6 heures)

3.1    Automates et machine: opérations et raisonnements

3.2    Diagrammes états/transitions

3.3    Diagrammes d’activités

4.    Spécifications, analyse et vérification de systèmes concurrents (12 heures)

4.1    AT et RdP : processus, exécution concurrente, objets partagés et exclusion mutuelle

4.2    AT et RdP : propriétés de vivacité et de sécurité, analyses, raisonnement

5.    Autres méthodes et approches - comparaison (3 heures)

5.1    Le langage Z, OCL et Alloy

5.2    UML exécutable

5.3    Vérification de modèles vs techniques de preuve

 


[1]   Ces heures sont des heures approximatives d’enseignement pour chaque sujet et incluent le temps alloué à l’examen intra-semestriel.




Évaluation
  1. Projet de spécification en 3 étapes (35%)
  2. Projet d'interprétation et de validation (15%)
  3. Examen (50%)



Dates des examens intra
Groupe(s) Date
1 3 aout 2017



Politique de retard des travaux
Tout travail (devoir pratique, rapport de laboratoire, rapport de projet, etc.) remis en retard sans motif valable, c’est-à-dire autre que ceux mentionnés dans le Règlement des études (1er cycle, article 7.2.7 b / cycles supérieurs, article 6.5.4 b) se verra attribuer la note zéro, à moins que d’autres dispositions ne soient communiquées par écrit par l’enseignant dans les consignes de chaque travail à remettre ou dans le plan de cours pour l’ensemble des travaux.

Dispositions additionnelles

  • La qualité du français sera prise en considération (jusqu'à 10 % de pénalité).
  • La remise de tous les travaux doit respecter les échéanciers fixés. La correction s’effectuant, dans plusieurs cas, le jour même de la remise, tout retard entraîne la note ZÉRO.
  • Une participation active des étudiants (es) est exigée. Jusqu’à 5% de la note finale sera retenue pour représenter cette participation. 



Absence à un examen
Dans les cinq (5) jours ouvrables suivant la tenue de son examen, l’étudiant devra justifier son absence d’un examen durant le trimestre auprès de la coordonnatrice – Affaires départementales qui en référera au directeur de département. Pour un examen final, l’étudiant devra justifier son absence auprès du Bureau du registraire. Toute absence non justifiée par un motif majeur (maladie certifiée par un billet de médecin, décès d’un parent immédiat ou autre) à un examen entraînera l’attribution de la note (0).



Plagiat et fraude
Les clauses du « Règlement sur les infractions de nature académique de l’ÉTS » s’appliquent dans ce cours ainsi que dans tous les cours du département. Les étudiants doivent consulter le Règlement sur les infractions de nature académique (https://www.etsmtl.ca/A-propos/Direction/Politiques-reglements/Infractions_nature_academique.pdf ) pour identifier les actes considérés comme étant des infractions de nature académique ainsi que prendre connaissance des sanctions prévues à cet effet.  À l’ÉTS, le respect de la propriété intellectuelle est une valeur essentielle et les étudiants sont invités à consulter la page Citer, pas plagier ! (https://www.etsmtl.ca/Etudiants-actuels/Baccalaureat/Citer-pas-plagier).



Documentation obligatoire

la documentation obligatoire sera disponible sur le site Moodle du cours.




Ouvrages de références

Language OCL: WARMER, Jos & KLEPPE, Anneke, The Object Constraint Language Getting your Models Ready for MDA. 2nd edition, Addison-Wesley, 2003. 




Adresse internet du site de cours et autres liens utiles

Les sites pertinents seront disponibles sur le site Moodle du cours.