Un assistant méthodologique UML Modélisation et vérification formelle de protocoles guidées par des patrons

摘要

La modélisation de services et protocoles est la clé de voûte de la validation d'une architecture de communication. L 'article propose de mener cette activité complexe dans le TURTLE Toolkit (TTool), environnement UML temps réel doté de capacités de vérification formelle. Les principes d'un assistant méthodologique pour l'analyse d'architecture de communication sont définis dans un cadre général, puis transposés à l'approche TTool sous la forme de patrons basés sur des cas d'utilisation et des scénarios paramétrables. L 'utilisation de ces patrons est illustrée sur un protocole de communication point à multipoint par satellite%Modeling services and protocols is a key point when the validation of a communication architecture is at stake. The paper proposes to address such a validation with the TURTLE Toolkit (Ttool), a UML-based environment with real-time modeling and formal verification capabilities. A pattern-based methodological assistant relying on UML analysis diagrams is defined and applied to Ttool. The patterns support parametrized use cases and scenarios. A space-based multicast communication system serves as example