Projet de spécification

MGL7160 Méthodes formelles et semi-formelles

Hiver 2001

Énoncé du problème

Pour ce travail, vous devez développer une spécification formelle en utilisant soit la notation Spec, soit la notation LOTOS. Selon la notation choisie, le système à spécifier sera différent et vous trouverez l'énoncé détaillé du problème à l'un des URLs indiqués ci-bas:

Spec: Spécification du modèle d'affaires d'un système de gestion de commandes par Internet:
```
   http://www.labunix.uqam.ca/~tremblay_gu/MGL7160/Projets/commandes
```
LOTOS: Spécification du comportement d'un système de surveillance des températures:
```
   http://www.labunix.uqam.ca/~tremblay_gu/MGL7160/Projets/temperatures
```

Note importante: Ce travail peut être fait seul ou avec une (1) autre personne.

Document à remettre et date limite de remise

La version finale de votre spécification est à remettre au plus tard le vendredi 4 mai à 12h00 (midi). Vous devrez me remettre une version sur papier (au secrétariat du département, soit dans la boîte de remise des travaux, soit par fax (987-4277), mais pas par courriel !).

Remarque importante: Dans le cas de la version Spec, votre spécification devra avoir été vérifiée à l'aide de l'analyseur Spec. (Voir la section 4 concernant l'utilisation de l'analyseur Spec.) Il est préférable de remettre une solution incomplète, mais valide au niveau de la syntaxe et des types, plutôt qu'une solution complète (sic ) mais incorrecte.

Version préliminaire

Vous pouvez (et vous devriez), avant la date finale de remise, me soumettre une version préliminaire (un brouillon, une version partielle) de votre spécification. J'examinerai ce document (sans lui attribuer de note) et je vous ferai part de mes commentaires ou suggestions, de façon à assurer que vous êtes sur la bonne voie. Notez que je pourrai recevoir vos documents préliminaires par courriel mais que je vous communiquerai mes commentaires uniquement en personne, soit en vous rencontrant, soit par téléphone (donc pas par courriel).

Dans le cas de la version Spec, la version préliminaire devrait présenter le squelette de votre module (interface des messages) sans donner les détails des transitions. Vous pouvez aussi indiquer le modèle conceptuel associé (avec les invariants appropriés), auquel cas je vérifierai s'il semble complet et correct. Toutefois, pour cette version préliminaire, je n'examinerai pas les détails de réponses et transitions.
Dans le cas de la version LOTOS, la version préliminaire devrait indiquer l'architecture générale de la solution (c'est-à-dire, l'expression qui donne la structure de haut niveau de votre système, préférablement accompagnée d'un diagramme indiquant les processus, leurs ports de communication et les liens entre ces ports), les en-têtes des divers processus, ainsi qu'une brève description informelle du rôle de chacun des processus.

Remarque: Comme je serai à l'extérieur du pays du 21 au 28 avril incl., je ne serai donc pas disponible durant cette péride pour répondre à vos questions ou pour vous donner mes commentaires sur une version préliminaire (même par courriel). Par contre, durant la semaine du 30 avril, je serai disponible pour consultation (sur rendez-vous), y compris le mardi soir, 1er mai, à l'heure habituelle du cours (à mon bureau: PK-4435) en autant que vous me contactiez au préalable pour prendre rendez-vous .

Utilisation de l'analyseur `Spec`

Comme votre spécification va très certainement comporter plusieurs modules, il pourrait être plus simple d'utiliser la version de l'analyseur disponible sur la machine arabica:

  http://www.labunix.uqam.ca/~tremblay_gu/utilisation-sur-arabica.html

Cette version de l'analyseur permet, lorsqu'un module m est analysé, de générer un fichier d'interface m.SpecInterf qui contient l'information nécessaire pour que les autres modules puissent ensuite utiliser les éléments exportés par le module m.

Si vous n'êtes pas familier avec l'utilisation de la machine arabica ou si vous n'avez pas de compte sur cette machine, vous pouvez utiliser la version suivante de l'analyseur, version qui permet elle aussi de générer un fichier d'interface pour un module:

   http://www.labunix.uqam.ca/~tremblay_gu/analyseur-spec-projet-7160.cgi

Notez toutefois que les fichiers d'interface ainsi générés sont véritablement publiques, c'est-à-dire que n'importe qui peut ensuite avoir accès à ces fichiers. De plus, si quelqu'un d'autre soumet un module du même nom, le fichier d'interface résultant écrasera alors un fichier d'interface déjà existant.

Pour examiner les fichiers d'interface disponibles, que vous avez créés ou que d'autres ont créés, il suffit d'accéder à l'URL suivant:

  http://www.labunix.uqam.ca/~tremblay_gu/bibliotheque-spec-7160.cgi

About this document ...

Projet de spécification

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

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

The translation was initiated by Tremblay Guy on 3/15/2001