Les langages SDL et MSC

Description

Cours 4TC –2006
Les langages SDL et MSC
Jean-Philippe Babau
INSA Lyon
[e-mail] 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)
[e-mail] CITI - IF - INSA 2Cours 4TC –2006
Plan
• Les langage SDL et MSC
– Principes
• Vérification, tests
• Génération de code
• UML / SDL
[e-mail] 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
[e-mail] 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
- ...

Sujets

• cours

Informations

• Publié par: Soug
• Nombre de lectures: 157
• Langue: Français

Extrait

Cours 4TC –2006  

Cours 4TC –2006  

Les langages SDL et MSC

Jean-Philippe Babau

INSA Lyon

[e-mail]  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)

[e-mail]  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

[e-mail]  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

[e-mail]  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  

[e-mail]  CITI - IF - INSA 5

Structure

[e-mail]  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] c2 c3 Block1 Block2 [s2] [s3] [s4]

Cours 4TC –2006  

[e-mail]  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 [e-mail]  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 s2 s3 s4 - e2

[e-mail]  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 *

[e-mail]  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 [e-mail]  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 [e-mail]  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 ; 㻱㻨㻺㻷㻼㻳㻨 㼆㼋㼄㼐㼓 㻶㻷㻵㻸㻦㻷 㻱㼘㼐 㻬㻱㻷㻨㻪㻨㻵㻞 㻹㼄㼏 㻨㻪㻨㻵㻞 㻬㻱㻷 㻧㻨㻩㻤㻸㻯㻷 㻋㻑 㻓㻏 㻓 㻑㻌㻞   㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞 㻱㻨㻺㻷㻼㻳㻨 㻷㼕㼄㼐㼈 㻤㻵㻵㻤㻼㻋㻬㼑㼇㼈㼛㻏 㼆㼋㼄㼐㼓㻌 㻨㻱㻧㻱㻨㻺㻷㻼㻳㻨㻞

㻧㻦㻯 㼘㼐㼈㼕㼒 㼌㼑㼗㼈㼊㼈㼕 㻝㻠 㻓 㻞 㼑 㻧㻦㻯 㻷㻔 㻷㼕㼄㼐㼈㻞  

[e-mail]  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)

[e-mail]  CITI - IF - INSA 16

Cours 4TC –2006  

㻷㻔㻋㻕㻌㻄㻱㼘㼐 㻝㻠 㻱㼘㼐㼈㼕㼒

[e-mail]  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

[e-mail]  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 [e-mail]  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 :

[e-mail]  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

     

[e-mail]  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

[e-mail]  CITI - IF - INSA 21

dcl X integer ; dcl Y integer;

Traitements amonts DemService() Ce signe veut dire que les messages * AttenteReponse c ( o s n o s it e  t r o v u é s s     s d a a u n f s     R la m  q e u s e s u a e g   e s ( a )  n )  s s  ê o t n r t e traités R DemService () * Traitements avals

Etat1 signal1 procedure Rep1 Etat2