Remerciez-le!

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

Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 1 Les langage

Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 1 Les langages SDL et MSC Jean-Philippe Babau INSA Lyon Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 2 Introduction • Modélisation – description abstraite – spécification, implantation • Validation / vérification – 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-fly) Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 3 Plan • Les langage SDL et MSC – Principes • Vérification, tests • Génération de code • UML / SDL Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 4 SDL : Specification and Description Language • Langage standard – Sémantique définie – Langage des télécom (ITU) – Langage normalisé (SDL 88, SDL 92, SDL 96, SDL2000) • Principes – Langage graphique et textuel – Machines à états finis communicantes • Outils – ObjectGéode, RTDS de PragmaDev, Tau de Télélogic – Edition – Vérification/Validation/test • MSC • observateurs – Génération de code Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 5 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) Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 6 Structure Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 7 Le system - Structure - block, canaux de communication - Déclaration des signaux, des types signal s1,s2(integer); signal s3,s4 ; System test Block1 Block2 c2 c1 c3 [s1] [s2] [s4] [s3] Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 8 Le block - Décomposition arborescente - substructure - Machine à état fini - process - 1 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 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 9 La communication Instance 1 de processus P Instance 1 de processus Q Instance 2 de processus P -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) Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 10 Description du comportement des process • Etat – Un état de départ obligatoire – Pas d’état hiérarchique – Pas d ’états concurrents – Un état de fin • Transition – Signal ou garde déclenchant – Corps • Appel de procedure, task • Alternatives • Émission de signaux – Retour dans un état • Identique ou différent • Hypothèse RTC « Run To Completion » – i-e transition non préemptible s1 Procedure1 val := … ; c s2 s2 s3 s4 e1 - e2 dcl val T_val ; Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 11 Description des process - Transition - (1) un signal non attendu est perdu sauf si sauvegarde explicite (save) du signal - (2) transition spontanée - (3) transition continue - (4) garde - (sauve s1 tant que x<3) - Facilité d’écriture - Tous les états, tous les signaux * S1 < x >3> none < x >3> (2) (3) (4) S1 (1) e1 e1 e1 e1 S1 * * e1 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 12 • PID – Type : pid – Identifiant du process : variable self • communication – Réception • pid de l’émetteur du dernier signal reçu : sender • Filtrage en réception : from – Émission • Destinataire explicite : to • Canal explicite : via • Création dynamique – dernier process créé : variable offspring – créateur : variable parent Gestion des identifiants de process Process2 Process2 Process1 Ack to sender s1 e1 e2 Ack via C1 s1 e1 e2 lePID = offspring PIDCreat = parent Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 13 Paramètres formels de process Process2(TRUE, 25) s1 e1 e2 FPAR etat BOOLEAN, Val INTEGER ; DCL … Process2 Process1 e1 Etat et Val sont initialisés à la création du process Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 14 Les données • Type Abstrait de données – Type prédéfinis (INTEGER, REAL, NATURAL, BOOLEAN, CHARACTER, CHARSTRING, DURATION, TIME, Pid, ARRAY, STRUCT, POWERSET) – SYNONYM, SYNTYPE, NEWTYPE, LITERALS • Données encapsulées – Propre à chaque instance de process – Déclaration : dcl val Type ; 㻧㻦㻯㻃㼑㼘㼐㼈㼕㼒㻃㼌㼑㼗㼈㼊㼈㼕㻃㻝㻠㻃㻓㻃㻞㻧㻦㻯㻃㻷㻔㻃㻷㼕㼄㼐㼈㻞㻶㻼㻱㻲㻱㻼㻰㻃㻱㼅㻱㼒㼇㼈㼖㻃㻠㻃㻔㻓㻞㻶㻼㻱㻷㻼㻳㻨㻃㻬㼑㼇㼈㼛㻃㻠㻃㻬㻱㻷㻨㻪㻨㻵㻦㻲㻱㻶㻷㻤㻱㻷㻶㻃㻔㻝㻱㼅㻱㼒㼇㼈㼖㻨㻱㻧㻶㻼㻱㻷㻼㻳㻨㻃㻞㻱㻨㻺㻷㻼㻳㻨㻃㼆㼋㼄㼐㼓㻶㻷㻵㻸㻦㻷㻱㼘㼐㻃㻬㻱㻷㻨㻪㻨㻵㻞㻹㼄㼏㻃㻬㻱㻷㻨㻪㻨㻵㻞㻧㻨㻩㻤㻸㻯㻷㻃㻋㻑㻃㻓㻏㻃㻓㻃㻑㻌㻞㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞㻱㻨㻺㻷㻼㻳㻨㻃㻷㼕㼄㼐㼈㻃㻤㻵㻵㻤㻼㻋㻬㼑㼇㼈㼛㻏㻃㼆㼋㼄㼐㼓㻌㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 15 Les données • Les opérateurs – Comparaison = /= > <= … – opérateurs logiques or and not xor – Opérateurs numériques + - * / – Affectation := – tableau make! extract! modify! • À utiliser uniquement dans les axiomes 㻱㼘㼐㼈㼕㼒㻃㻝㻠㻃㻗㻷㻔㻋㻕㻌㻄㻱㼘㼐㻃㻝㻠㻃㻱㼘㼐㼈㼕㼒㻷㻔㻋㻔㻌㻄㻹㼄㼏㻃㻒㻠㻃㻔㻱㼘㼐㼈㼕㼒㻃㻡㻃㻖㻃㼄㼑㼇㻱㼘㼐㼈㼕㼒㻃㻟㻃㻘 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 16 Les actions • Task – Affectations • Appel de procédure – Local – Distant • Émission implicite d’un signal • état implicite d’attente • RPC • Conditionnelles Val1 := v0, Val2 : = v1 Suivant(3,4,I) B := call Suivant(4,4,J) expbooléenne (TRUE) (FALSE) valeur (1) (ELSE) (2) Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 17 Les actions • Labels – Utiles pour les boucles – goto : à éviter I := 0 I = N (TRUE) (FALSE) I := I + 1 suiv suiv Action Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 18 SDL exemple tache (2,2) ressource (1,1) [Dem,Libere] [OK] libre Dem occupant := SENDER OK to SENDER occupe DCL occupant PID ; DCL bloque PID ; occupe Dem bloque := SENDER occupe occupe Libere OK to occupant occupe libre occupant = null occupant = bloque bloque = null bloque = null (TRUE) (FALSE) Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 19 SDL exemple • si Libere quand libre : ? • si re-demande : ? • si libere par mauvaise tâche : ? • état occupe / demande : ? • si plusieurs tâches : ? Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 20 Description de procédures • Déclaration • Algorithme – Début – Fin – État • Paramètres formels – Entrée : IN – Entrée/sortie : IN/OUT – Retour : RETURNS Suivant FPAR IN Index1 INTEGER, Taille INTEGER, IN/OUT Index2 INTEGER; RETURNS BOOLEAN ; DCL … Index2=Index1 + 1 Index1= Taille (TRUE) (FALSE) Index2 = 1 TRUE FALSE Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 21 Description de procédures procedure lireCapteur fpar in / out X integer, procedure lireCapteur; fpar : returns X integer ; external ; X:= call lireCapteur() dcl X integer ; dcl Y integer; • Appel de procédure externe C – Signature – Simulation • Génération de code • Édition de lien Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 22 Description de procédures DemService() AttenteReponse R DemService () * Ce signe veut dire que les messages * (soit tous sauf Rmessage() ) sont conservés dans la queue sans être traités Traitements amonts Traitements avals procedure signal1 Rep1 Etat1 Etat2 • État implicite du process Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 23 Les données partagées • Modèles de partage – revealed/view • multi-lecteur/mono-écrivain, partage d’une donnée entre 2 processus d’un même bloc – export/import + remote • multi-lecteur/multi-écrivain, i1P1.d1 dcl exported d1 integer; export(d1) d4 := import(d1,pidi1P1) imported d1 integer; dcl d4 integer; dcl pidi1P1 pid; export(d1) P2 P1 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 24 SDL et le temps • Données – Deux types prédéfinis: Time et Duration – Estampille locale en utilisant Now • Timer (temporisateur ) – Déclaré et utilisé par un seul process – Actions : Armer ( set ), Arrêter (reset) – Attente d’un signal timer reveil1 := 10 ; timer reveil2 ; reveil1 set (reveil1); set (now + 100, reveil2); reset (reveil1); Now +10 Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 25 SDL et les types • Héritage simple • Types paramétrés – Paramètre formel de contexte • System, block – Procédure, signal, synonyme, type de données • Process – Process, procédure, signal, synonyme, type de données • Procédure – Process, procédure, signal, synonyme, variable, réveil type de données – Type non paramétré • Instance de type non paramétré • Spécialisation (inherits) – Ajout – Modification (virtual / redefined) • Block, processus, procedure, transition TP TNP Inst Cours 4TC –2006 jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 26 Vérification ( Objectgéode ) • Simulation – Point d'arrêt sur conditions (états, valeurs) – Mode pas à pas : mise au point – Mode aléatoire : test – Mode simulation exhaustive • uploads/Management/ les-langages-sdl-et-msc.pdf