Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Les langages sdl et msc Cours TC ?? Les langages SDL et MSC Jean-Philippe Babau INSA Lyon jean-philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? Introduction ? Modélisation ?? description abstraite ?? spéci ?cation implantation ? Validation véri ?c

Cours TC ?? Les langages SDL et MSC Jean-Philippe Babau INSA Lyon jean-philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? Introduction ? Modélisation ?? description abstraite ?? spéci ?cation implantation ? Validation véri ?cation ?? propriété du cahier des charges ?? propriétés applicatives absence de deadlock ? ?? analyse de performance ? Langages formels ?? sémantique non ambigu? ?? LOTOS Estelle SDL ? Techniques de validation ?? Simulation exhaustive aléatoire test ?? Preuves logiques temporelles model-checking on-the- y jean-philippe babau insa-lyon fr CITI - IF - INSA CCours TC ?? Plan ? Les langage SDL et MSC ?? Principes ? Véri ?cation tests ? Génération de code ? UML SDL jean-philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? SDL Speci ?cation and Description Language ? Langage standard ?? Sémantique dé ?nie ?? Langage des télécom ITU ?? Langage normalisé SDL SDL SDL SDL ? Principes ?? Langage graphique et textuel ?? Machines à états ?nis communicantes ? Outils ?? ObjectGéode RTDS de PragmaDev Tau de Télélogic ?? Edition ?? Véri ?cation Validation test ? MSC ? observateurs ?? Génération de code jean-philippe babau insa-lyon fr CITI - IF - INSA CCours TC ?? Principes généraux Décomposition arborescente system block substructure process procedure Communication Canaux de communication canaux et routes - Signaux avec paramètres optionnels Comportement dans les process et les procédures Typage des données ADT Abstract Data Type jean-philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? Structure jean-philippe babau insa-lyon fr CITI - IF - INSA CCours TC ?? Le system Structure block canaux de communication Déclaration des signaux des types ? ? ? ? ? ? ? ? ? System test c s Block c s signal s s integer signal s s c Block s s jean-philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? Le block Décomposition arborescente substructure Machine à état ?ni process - ou plusieurs instances un PID par instance i j création statique de i instances et j nb max de création dynamique d ? instances Exécution parallèle des process Communication par les routes Déclarations Signaux internes - procedure types jean-philippe babau insa-lyon fr CITI - IF - INSA CCours TC ?? La communication -Communication asynchrone par signal Le signal véhicule des paramètres - Emis par une instance de process - Destinataire une instance ou toutes les instances - un seul consommateur indéterministe - gestion en FIFO sauf si signal prioritaire priority Instance de processus P Instance de processus P Instance de processus Q jean- philippe babau insa-lyon fr CITI - IF - INSA Cours TC ?? Description du comportement des process ? Etat ?? Un état de départ obligatoire ?? Pas d ? état hiérarchique ?? Pas d ? états concurrents ?? Un état de ?n ? Transition ?? Signal ou garde déclenchant ?? Corps ? Appel de procedure task ? Alternatives ? Émission de signaux ?? Retour dans un état ? Identique ou di ?érent ? Hypothèse