NB: ce document est disponible à: http://bobolink.homeip.net/~robertjo/TEL233/index.html
NB: les informations mentionnées ici changent constamment !
NB: dernière mise à jour: 03/11/26

TEL300: problèmes spéciaux

"Modélisation et analyse logique:
architectures et protocoles informatiques"

janvier 2004

Prof. Robert deB. Johnston

Introduction

Le cours fournit des techniques mathématiques et des outils informatiques pour la modélisation et l'analyse d'architectures et de protocoles informatiques. La modélisation se situe au niveau de la logique des comportements. Les techniques mathématiques incluent la théorie des ensembles, la logique du premier ordre, et la logique temporelle. L'outil informatique principal est l'ensemble de programmes pour TLA+ de Leslie Lamport, en particulier le programme TLC. TLC fait une analyse logique des modèles et des propriétés exprimées via le langage TLA+. Un résultat positif équivaut à une preuve exhaustive, c.a.d. une démonstration mathématique, qu'un modèle satisfait toutes ses spécifications.

L'approche est importante dans le contexte d'études de systèmes où il y a plusieurs activités simultanées, par exemple, les systèmes d'exploitation, les systèmes répartis, et les protocoles de communication. C'est difficile d'imaginer toutes les intéractions possibles et leurs effets. Ce cours est donc offert en parallèle au cours TEL222, "Ingénerie des Systèmes Répartis", le but étant de maximiser la synérgie entre les deux.

A la fin du cours, l'étudiant(e) aura une appréciation de, et un porte-feuille d'approches et d'outils pour, la conception et la réalisation rigoureuses de systèmes numériques.

Auditeurs Visés

Tout ceux qui ont interêt à produire des "designs" correctes.

Prérequis

  1. Une connaisssance minime de la théorie des ensembles et de la logique
  2. Un ordinateur personnel (Windows, Macintosh, Linux).

Texte

Leslie Lamport, "Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers", Addison-Wesley Pearson, 2003, ISBN 0-321-14306-X.

Une version .pdf de ce texte est disponible sans frais à partir de la page d'acceuil de TLA+ citée ci-bas.

Références

  1. Page d'accueil de TLA+ : http://research.microsoft.com/users/lamport/tla/tla.html
  2. Liste des exemples du cours: http://bobolink.homeip.net/~robertjo/TEL233/TLA/index.html
  3. Radia Perlman, "Interconnections: Bridges, Routers, Switches, and Internetworking Protocols", ed 2, Addison-Wesley Longman, 2000, ISBN 0-201-63448-1.

Sujets traités

  1. L'outillage TLA+
    1. Obtention et installation des outils
    2. Survol des outils
      1. SANY: l'analyseur syntaxique
      2. TLC: le vérificateur
      3. TLATEX: le formatteur
    3. Exemples préliminaires
    4. Plan général d'attaque
  2. Syntaxe et sémantique de TLA+
    1. TLA: variables, états, actions, et comportements
    2. Un premier concept de spécification: les Invariants
    3. Exemple: spécifications d'un horloge (tla1|pdf1|cfg1), (tla2|pdf2|cfg2)
    4. Exemple: une interface asynchrone
    5. Exemple: un FIFO
    6. Autres concepts de spécification
      1. Implantation
      2. Guaranties de progrès (vivacité)
    7. La logique et la théorie des ensembles (ZFC) en TLA+
    8. Définitions et le rôle des Modules
  3. Modélisation et analyse de systèmes: les Invariants
    1. Concepts de base
    2. L'algorithme d'Euclide
    3. Recherche par dichotomie
    4. L'exclusion mutelle
      1. L'algorithme de Dekker
      2. L'algorithme de Peterson
    5. Mémoires "caches"
      1. Les exemples de Lamport
      2. La cache "Least Recently Used (LRU)"
    6. Protocoles de communication
      1. Le protocole "Bit Alterné"
      2. Le protocole RLP
    7. Structures des données
      1. Listes doublement chaînées
  4. Modélisation et analyse de systèmes: Implantation/Raffinement
    1. Concepts de base
    2. Vérification d'un circuit numérique (addition)
    3. Listes doublement enchainées
  5. Modélisation et analyse de systèmes: Guaranties de Progrès
    1. Concepts de base
    2. La "Write-Through cache"
    3. Le tampon formel, mais animé, de P. Ladkin
  6. Etudes de cas
    1. Banques de données réparties
    2. Ponts entre réseaux locaux
    3. L'algorithme OSPF
    4. Noyau d'un système d'exploitation
    5. Géstion des Threads sous Windows
  7. Conclusion

Evaluation

Exercices (travaux pratiques) + choix entre une synthèse ou un projet. Les exercices et le choix de sujet seront co-ordonnés entre ce cours et TEL222.