MGL7160 Méthodes formelles et semi-formelles
Syllabus
Hiver 2001

``The central activity of software development is description. Software developers need to master the techniques of description, and to understand what makes a particular description suitable or unsuitable for a particular purpose. [...] If you understand how descriptions work, and how one description differs from another, you can use this understanding to improve your thinking about problems. Thinking about descriptions is thinking about thinking.''
M. Jackson [Jac95]

``If you can't write down a mathematical description of the behaviour of the system you are designing then you don't understand it. [...] If that is the case, what are you doing entrusting people's lives to that system because by definition you don't understand how it's going to behave under all circumstances?''
M. Thomas [BS93]

``... if you want to build systems with ultra-high reliability which provide very complex functionality and you want a guarantee that they are going to work with this very high reliability ... you can't do it!''
B. Littlewood [BH95a]

Professeur:

Guy Tremblay

Local:

PK-4435

Téléphone:

987-3000 poste 8213#

Email:

tremblay.guy@uqam.ca

Page web du cours:

http://www.labunix.uqam.ca/~tremblay_gu/MGL7160

Horaire du cours:

Mardi 17:30 - 20:30 (local SH-3360)

Mardi 20 février: Pas de cours (semaine de relâche de la famille des sciences).

Description (selon l'annuaire)

Introduction à certaines notations formelles pour décrire les exigences et les spécifications de systèmes logiciels. Méthodes pour les systèmes séquentiels (tel que le langage Z ou la notation de Mills) et pour les systèmes concurrents et réactifs (tels que les machines d'états et les réseaux de Petri avec certaines extensions concernant les données). Utilisation des méthodes formelles pour l'analyse des propriétés et du fonctionnement des systèmes au niveau de la spécification, de la conception ou de l'implantation.

Objectifs

Généraux:
Le cours vise à initier les étudiant-e-s aux méthodes formelles et à leur rôle dans le cycle de développement des logiciels; il vise aussi à faire comprendre les avantages et les limites de ces méthodes.

Spécifiques:
À la fin du cours, l'étudiant-e devrait être capable ...

• d'expliquer le rôle des méthodes formelles dans le cycle de vie des logiciels;
• de lire et écrire des exemples de spécifications formelles dans diverses notations;
• d'identifier les avantages et limites de l'utilisation des méthodes formelles;
• d'évaluer et juger de l'opportunité d'utiliser ou non des méthodes formelles pour divers types d'applications.

Formules pédagogiques

• Exposés magistraux
• Exercices (en classe et à la maison)
• Travail pratique de spécification d'un logiciel
• Lectures d'articles et discussions/exposés

Contenu du cours

• Motivation et justification des méthodes formelles.
• La notation SPEC (modélisation abstraite):
  • Logique, concepts et modules de définition, formalisation du domaine d'application;
  • Types abstraits: ensembles, séquences, dictionnaires;
  • Modules pour les spécifications fonctionnelles: fonctions, machines, types;
• La notation LOTOS (pour les systèmes réactifs et concurrents):
  • Actions, transitions et processus;
  • Équivalences entre processus;
  • Spécification et vérification de propriétés;
• Autres notations: VDM et Z, OCL (Object Constraint Language).
• Méthode rigoureuse de développement et obligations de preuve: cohérence interne, satisfaisabilité, raffinements.
• Sujet divers (exposés faits par les étudiant-e-s)

Évaluation (À discuter)

+ Exercices [30 %]: exercices à faire à la maison et à remettre la semaine suivante (n parmi m, n << m);

+ Résumé [15 %]: lecture et résumé d'un article décrivant un projet industriel ayant utilisé des méthodes formelles (formulaire à remplir sur le web );

+ Travail pratique [25 %]: travail de spécification (SPEC ou LOTOS) d'un système de gestion ou d'un système réactif et concurrent;

+ Exposé et résumé [30 %]: résumé écrit [10 %] et présentation orale [20 %] sur un sujet au choix (approuvé par le prof.) lié aux méthodes formelles (2 pages, 20-30 minutes);

Remarques

* Les exercices et le travail pratique pourront être réalisés individuellement ou avec une (1) autre personne. L'exposé oral et les résumés devront être faits individuellement.

* La qualité du français sera prise en considération (jusqu'à 10% de pénalité).

Matériel

Manuel (en vente à la COOP-Sciences):

G. Tremblay. Modélisation et spécification formelle des logiciels. Loze-Dion Éditeurs, Inc., Montréal, Qué., 2 ième trimestre 2000.

D'autres notes de cours (sur les systèmes réactifs et concurrents et le langage LOTOS) ainsi que des photocopies d'articles vous seront distribuées au cours de la session.

Site Web: Un site Web consacré au cours MGL7160 sera accessible tout au long de la session. L'adresse de ce site est la suivante:

  http://www.labunix.uqam.ca/~tremblay_gu/MGL7160

References

AI91

D. Andrews and D. Ince.
Practical formal methods with VDM.
McGraw-Hill, 1991.
[En réserve: QA76.76D47A54].

BH95a

J. Bowen and M.G. Hinchey.
Seven more myths of formal methods.
IEEE Software, 12(4):34-41, July 1995.

BH95b

J. Bowen and M.G. Hinchey.
Ten commandments of formal methods.
IEEE Computer, 28(4):56-63, April 1995.

BL91

V. Berzins and Luqi.
Software Engineering with Abstractions.
Addison-Wesley Publishing Co., 1991.
[En réserve: QA76.76D47B47].

BS93

J. Bowen and V. Stavridou.
The industrial take-up of formal methods in safety-critical and other areas: A perspective.
In FME '93: Industrial-Strength Formal Methods, pages 183-195. Springer-Verlag, LNCS-670, 1993.

CGR95

D. Craigen, S. Gerhart, and T. Ralston.
Formal methods reality check: Industrial usage.
IEEE Trans. on Soft. Eng., 21(2):90-98, Feb. 1995.

GCR94

S. Gerhart, D. Craigen, and T. Ralston.
Experience with formal methods in critical systems.
IEEE Software, 11(1):21-28, Jan. 1994.

GH93

J.V. Guttag and J.J. Horning.
Larch: Languages and Tools for Formal Specification.
Springer-Verlag, 1993.
[En réserve: QA76.6G88].

Gib94

W.W. Gibbs.
Software's chronic crisis.
Scientific American, 271:86-95, Sept. 1994.

Hal90

A. Hall.
Seven myths of formal methods.
IEEE Software, 7(5):11-19, Sept. 1990.

Jac95

M. Jackson.
Software Requirements & Specifications -- a lexicon of practice, principles and prejudices.
ACM Press & Addison-Wesley, 1995.

Jon92

C.B. Jones.
VDM: Une méthode rigoureuse pour le développement du logiciel.
Masson, 1992.
[En réserve: QA76.76D47J6514].

Tur93

K.J. Turner.
Using formal description techniques: an introduction to Estelle, LOTOS, and SDL.
J. Wiley & Sons, 1993.
[En réserve: QA76.6U85].

WK99

J. Warmer and A. Kleppe.
The Object Constraint Language -- Precise Modeling with UML.
Addison-Wesley, 1999.

Wor92

J.B. Wordsworth.
Software development with Z: a practical approach to formal methods in software engineering.
Addison-Wesley, 1992.
[En réserve: QA76.73Z2W67].

Remarque: Une bibliographie détaillée (commentée) est disponible à l'URL suivant:

    http://www.labunix.uqam.ca/~tremblay_gu/chercher-reference.cgi

About this document ...

MGL7160 Méthodes formelles et semi-formelles
Syllabus
Hiver 2001

This document was generated using the LaTeX2HTML translator Version 97.1 (release) (July 13th, 1997)

Copyright © 1993, 1994, 1995, 1996, 1997, Nikos Drakos, Computer Based Learning Unit, University of Leeds.

The command line arguments were:
latex2html -split +0 -auto_navigation syllabus.tex.

The translation was initiated by Tremblay Guy on 1/11/2001