Les langages SDL et MSC
18
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
18
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Cours 4TC –2006
Les langages SDL et MSC
Jean-Philippe Babau
INSA Lyon
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 1
Cours 4TC –2006
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)
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 2 Cours 4TC –2006
Plan
• Les langage SDL et MSC
– Principes
• Vérification, tests
• Génération de code
• UML / SDL
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 3
Cours 4TC –2006
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
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 4 Cours 4TC –2006
Principes généraux
- Décomposition arborescente
- system, block, substructure, process, procedure
- Communication
- Canaux de communication (canaux et routes)
- Signaux avec paramètres optionnels
- ...
Voir
Les langages SDL et MSC
Jean-Philippe Babau
INSA Lyon
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 1
Cours 4TC –2006
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)
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 2 Cours 4TC –2006
Plan
• Les langage SDL et MSC
– Principes
• Vérification, tests
• Génération de code
• UML / SDL
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 3
Cours 4TC –2006
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
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 4 Cours 4TC –2006
Principes généraux
- Décomposition arborescente
- system, block, substructure, process, procedure
- Communication
- Canaux de communication (canaux et routes)
- Signaux avec paramètres optionnels
- ...
Cours 4TC –2006
Cours 4TC –2006
Les langages SDL et MSC
Jean-Philippe Babau
INSA Lyon
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 1
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)
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 2
Cours 4TC –2006
• Les langage SDL et MSC – Principes • Vérification, tests • Génération de code • UML / SDL
Cours 4TC –2006
Plan
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 3
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
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 4
Cours 4TC –2006
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 5
Structure
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 6
Cours 4TC –2006
Le system
- Structure -block , canaux de communication - Déclaration des signaux, des types
System te c s 1 t signal s1,s2(integer); signal s3,s4 ; [s1] c2c3 Block1 Block2 [s2] [s3] [s4]
Cours 4TC –2006
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 7
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
jea
Cours 4TC –2006
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 1 de processus P
Instance 2 de processus P Instance 1 de processus Q jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 9
Cours 4TC –2006 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
dcl _ l ; val T va e1 s1 s2 Procedure1 val := … ; c s2s3 s4 -e2
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 10
Cours 4TC –2006
Description des process
- Transition - (1) un signal non attendu est perdu sauf si sauvegarde explicite ( save ) du signal e1 e1 e1 e1 - (2) transition spontanée S1 none < x >3 > S1 - (3) transition continue < x >3 > - (4) garde (1) (2) (3) (4) - ( sauve s1 tant que x<3 )
- Facilité d’écriture - Tous les états, tous les signaux *
Cours 4TC –2006
* S1
e1 *
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 11
Gestion des identifiants de process
• PID 1 e1 e – Type : pid – Identifiant du process : variable self s1 s1 • communication Ack to sender Ack via C1 – Réception • pid de l’émetteur du dernier signal reçu : sender e2 e2 • Filtrage en réception : from – Émission • Destinataire explicite : to • Canal explicite : via Process1 Process2 • Création dynamique lePID = offspring – dernier process créé : variable offspring – créateur : variable parent Process2 PIDCreat = parent jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 12
Cours 4TC –2006
Paramètres formels de process
Process1
e1 s1 Process2(TRUE, 25) e2
Process2
FPAR etat BOOLEAN, Val INTEGER ; DCL …
e1 Etat et Val sont initialisés à la création du process jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 13
Cours 4TC –2006 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, LITERA 㻶㻼㻱㻲㻱㻼㻰 㻱㼅㻱㼒㼇㼈㼖 㻠 㻞 㻔㻓 • Données encapsulées 㻶㻼㻱㻷㻼㻳㻨 㻬㼑㼇㼈㼛 㻠 㻬㻱㻷㻨㻪㻨㻵 – Propre à chaque instance de process 㻦㻨㻱㻲㻧㻱㻶㻶㻼㻷㻱㻤㻷㻱㻼㻷㻳㻶 㻨㻔 㻞㻝㻱㼅㻱㼒㼇㼈㼖 – Déclaration : dcl val Type ; 㻱㻨㻺㻷㻼㻳㻨 㼆㼋㼄㼐㼓 㻶㻷㻵㻸㻦㻷 㻱㼘㼐 㻬㻱㻷㻨㻪㻨㻵㻞 㻹㼄㼏 㻨㻪㻨㻵㻞 㻬㻱㻷 㻧㻨㻩㻤㻸㻯㻷 㻋㻑 㻓㻏 㻓 㻑㻌㻞 㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞 㻱㻨㻺㻷㻼㻳㻨 㻷㼕㼄㼐㼈 㻤㻵㻵㻤㻼㻋㻬㼑㼇㼈㼛㻏 㼆㼋㼄㼐㼓㻌 㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞
㻧㻦㻯 㼘㼐㼈㼕㼒 㼌㼑㼗㼈㼊㼈㼕 㻝㻠 㻓 㻞 㼑 㻧㻦㻯 㻷㻔 㻷㼕㼄㼐㼈㻞
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 14
expbooléenne valeur (TRUE) (FALSE) (1) (2) (ELSE)
• Task – Affectations • Appel de procédure – Local – Distant • Émission implicite d’un signal • état implicite d’attente • RPC
• Conditionnelles
㻷㻔㻋㻔㻌㻄㻹㼄㼏 㻒㻠 㻔 㻱㼘㼐㼈㼕㼒 㻝㻠 㻗
• 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
Les données
Les actions
Val1 := v0, Val2 : = v1 Suivant(3,4,I) B := call Suivant(4,4,J)
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 16
Cours 4TC –2006
㻷㻔㻋㻕㻌㻄㻱㼘㼐 㻝㻠 㻱㼘㼐㼈㼕㼒
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 15
㻱㼘㼐㼈㼕㼒 㻡 㻖 㼄㼑㼇 㻱㼘㼐㼈㼕㼒 㻟 㻘
Cours 4TC –2006
Les actions
• Labels – Utiles pour les boucles I := 0 – goto : à éviter suiv I = N (TRUE) (FALSE) Action I := I + 1 suiv
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 17
Cours 4TC –2006 SDL exemple [Dem,Libere] tache ressource (2,2) [OK] (1,1) libre occupe occupe Dem Dem Libere occupant := SENDER bloque := SENDER OK to SENDER bloque = null occupe occupe (TRUE) (FALSE) occupant = null occupant = bloque DCL occupant PID ; libre bloque = null e PID ; DCL bloqu OK to occupant occupe jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 18
Cours 4TC –2006
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
• Déclar • Algorit – Dé – Fin – Éta
• Paramètre – Entrée : – Entrée/ – Retour :
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 19
Description de procédures
Suivant
FPAR IN Index1 INTEGER, Taille INTEGER, IN/OUT Index2 INTEGER;
Inde TRUE ean-p ppe. a au
FALSE
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 22
• État implicite du process
Description de procédures
Cours 4TC –2006
Cours 4TC –2006 Description de procédures • Appel de procédure externe C – Signature – Simulation • Génération de code • Édition de lien
procedure lireCapteur fpar in / out X integer, procedure lireCapteur; fpar : X:= call lireCapteur() rexttuerrn ; s l X integer ; e na
jean-philippe.babau@insa-lyon.fr CITI - IF - INSA 21
dcl X integer ; dcl Y integer;
Traitements amonts DemService() Ce signe veut dire que les messages * AttenteReponse c(osnosite trovuéss sdaaunfs Rlam qeusesuaeg es(a) n) ss êotnrte traités R DemService () * Traitements avals
Etat1 signal1 procedure Rep1 Etat2
