Nous développons une méthode de modélisation et de validation adaptée aux système parallèles structurés en couches hiérarchiques. Nous définissons deux notions : la concordance de modèle prouve que le modèle possède bien les propriétés dégagées par les spécifications; l'adéquation de service valide le protocole par rapport à son service. Nous appliquons notre méthode à la modélisation du protocole de télécommunication de niveau Transport (la couche 4 d'après la norme ISO sur l'interconnexion des systèmes ouverts). Nous étudions tout particulièrement la gestion de désynchronisations du Service de la couche Réseau, et le contrôle de flux avec réquisition de crédit du protocole de la couche Transport. Nous utilisons les réseaux de Petri à prédicats pour décrire le modèle du service rendu par le couche Réseau sous-jacente et nous en servir pour construire le modèle du protocole de ma couche Transport. nous prouvons que la notion d'abstraction peut s'étendre aux réseaux de Petri à prédicats. La preuve du déroulement correct du protocole est apportée en utilisant les invariants issus du modèle.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00864063 |
| Date | 09 April 1987 |
| Creators | Cousin, Bernard |
| Publisher | Université Pierre et Marie Curie - Paris VI |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0048 seconds