[PDF] Processus de transformation MDA dun schéma conceptuel de

View - Download Processus de transformation MDA dun schéma conceptuel de

Previous PDF

Next PDF

N od'ordre : 291

Centrale Lille

TH ESE presentee en vue d'obtenir le grade de

DOCTEUR

en Specialite : Automatique, Genie Informatique, Traitement du Signal et Images par

Rahma YANGUI ep BEN AYED

DOCTORAT DELIVR

E PAR CENTRALE LILLE

Titre de la these :

Modelisation UML/B pour la validation des exigences de securite des regles d'exploitation ferroviaires Soutenue le 19 fevrier 2016 devant le jury d'examen :

PresidentPr, Yves LEDRU LIG, Grenoble

RapporteurPr, Catherine DUBOIS ENSIIE, Evry

RapporteurMCF-HDR, Mohamed SALLAK UTC, Compiegne

MembreDirecteur R&D, Thierry LECOMTE Clearsy, Aix en Provence

MembreDr, Agnes LANUSSE CEA-List, Saclay

MembrePr, Pascal YIM ECL, Lille

Directeur de theseDR, Simon COLLART-DUTILLEUL IFSTTAR, Lille

EncadrantCR, Philippe BON IFSTTAR, Lille

These preparee dans le Laboratoire d'

Evaluation des Systemes de Transports

Automatises et de leur Securite

IFSTTAR, COSYS/ESTAS, Villeneuve d'Ascq

Ecole Doctorale SPI 072 (EC Lille)

i

Remerciements

Les travaux de these presentes dans ce manuscrit ont ete realises a l'institut francais des sciences et technologies des transports, de l'amenagement et des reseaux (IFSTTAR) a Villeneuve d'Ascq. Je tiens tout d'abord a remercier IFSTTAR de m'avoir oert cette experience magnique. La recherche scientique est un metier magique et c'est un bonheur de l'avoir commence ici. C'est avec toute ma profonde gratitude que j'exprime mes sinceres remerciements a mon directeur de theseSimon Collart-Dutilleuld'avoir diriger ce travail de these. Sans sa disponibilite malgre sa charge de travail, sa patience, les conseils qu'il m'a prodigues tout au long de ces trois ans, ses mots d'encouragement, ce travail n'aurait pas pu, sans doute, ^etre mene a son terme. Merci. J'exprime ma profonde reconnaissance et remerciement a mon encadrantPhilippe Bon d'avoir encadre ce travail de these, pour son soutien, ses conseils et sa participation dans l'accomplissement de ce travail de these. Merci. Je remercie chaleureusement MessieursYves LedruetAkram Idani, qui ont suivi de pres ce travail, sans qui cette partie n'existerait pas sous cette forme. Leurs observations judicieuses et leurs remarques ont ete des plus determinantes dans la conduite de ces tra- vaux. Merci. Mes vifs remerciements vont aussi a MadameCatherine Dubois, Professeur de l'Ecole Nationale Superieure d'Informatique pour l'Industrie et l'Entreprise a Evry et Monsieur Mohamed Sallak, Ma^tre de conference HDR de l'universite de Technologie de Compiegne, pour avoir accepte d'examiner ce travail en qualite de rapporteurs. Je tiens egalement a exprimer ma gratitude a MessieursYves Ledru, Professeur de l'universite Joseph Fourier a Grenoble, etPascal Yim, Professeur de l'Ecole centrale de Lille, et MadameAgnes La- nusse, Ingenieur-Chercheur du CEA-List a Saclay, pour avoir accepte de faire partie du jury en qualite d'examinateurs, ainsi que MonsieurThierry Lecomteen qualite d'invite. Mes remerciements vontegalement a tous les personnels du centre IFSTTAR-Villeneuve d'Ascq pour la gentillesse et la convivialite dont ils ont fait preuve et qui ont rendu mon sejour tres agreable parmi eux. Je remercie chaleureusement mes amiesHajer Sassi,Imen Chakroun,Sana Cherif, Hana Krichen,Chiraz Trabelsi,Karima Boufaras,Amira Bradai,Mouna Walha,Fatiha Azmani,Manel Hmimida,Amira Arouspour leurs soutiens et leurs encouragements. ii J'ai une pensee toute particuliere a ma famille pour leur soutien et leur amour. Tout ca n'aurait jamais ete possible sans le soutien inconditionnel de mes parentsSondesset Anouar, qui ont toujours cru en moi. Merci pour avoir fait de moi ce que je suis a present. Merci a mes cheres sursAmenietNourpour leurs conseils et leurs encouragements dans les moments diciles. Cette etape de ma vie n'aurait pas ete la m^eme sans la presence et l'amour de mon cher mariMohamed.Mohamed, je te remercie de tout mon cur d'^etre patient et souriant, de me soutenir et de m'encourager a aller plus loin et a franchir les dicultes tout en etant er de moi. Je remercie egalement mon cher lsRayenqui apporte toujours la joie de vivre au sein de ma petite famille. Par cette occasion, je remercie ma belle famille : mes beaux parentsSarraetAbdelmajidet ma belle surNadiapour leur soutien et leurs encouragements. Je dedie tout ce travail a mon cher lsRayenet a ma futur lle ..., les plus chers a mon cur. En dernier, je remercie tous ceux qui m'ont aide de pres ou de loin a realiser cette these.

Table des matieres

1 Introduction generale

3

1.1 Contexte scientique

4

1.2 Contexte industriel

5

1.2.1 Le systeme

ER TMS

5

1.2.2 Le projetPERFECT. . . . . . . . . . . . . . . . . . . . . . . . . . .8

1.3 Problematique de la these

9

1.3.1 Specication de la reglementation

10

1.3.2 La verication et la validation formelles

11

1.4 Motivations et contributions

12

1.5 Organisation du memoire

14

I CONTEXTE ET

ETAT DE L'ART17

2 Contexte scientique

19

2.1 Introduction

20

2.2 Ingenierie Systeme

20

2.2.1 Ingenierie des exigences

21

2.2.2 Exigences de S^urete de Fonctionnement et cadre normatif

22

2.2.2.1 Securite-innocuite

24

2.2.2.2 Securite-condentialite

25

2.3 Ingenierie dirigee par les modeles

26

2.3.1 Du

tout est objetvers letout est modele. . . . . . . . . . .26

2.3.2 Concepts de base de l'

IDM 28

2.3.2.1 Meta-modele et langage de modelisation

28

2.3.2.2 Meta-meta-modele et langage de meta-modelisation

29

2.3.3 L'approche

MD A 30

2.3.4 La transformation de modeles

32

2.3.5 Verrous scientiques en

IDM 34

2.3.5.1 La construction des modeles

34

2.3.5.2 L'heterogeneite des modeles et des meta-modeles

35

2.3.5.3 La denition des meta-modeles

35

2.3.5.4 L'evolution des meta-modeles

36

2.4 Mise en application de l'

IDM 37
2.4.1 IDM dans l'industrie des syst emescritiques 37
2.4.2 IDM p ourles syst emesferro viaires 38
iv Table des matieres

2.4.2.1 Le projet CECRIS

38

2.4.2.2 Le projet OpenETCS

40

2.4.2.3 Autres projets

41

2.4.3 Synthese sur la mise en application de l'

IDM 43

2.5 Synthese

44

3 Couplage de specications en

UML et B 45

3.1 Introduction

46

3.2 Specication

46

3.2.1 Denition et objectifs

47

3.2.2 Dierents types de langage de specication

47

3.2.2.1 Langages naturels

48

3.2.2.2 Langages semi-formels

48

3.2.2.3 Langages formels et methodes formelles

49

3.3 Verication et validation

50

3.3.1 Denitions

50

3.3.2 Techniques de verication et de validation

51

3.3.2.1Model checking. . . . . . . . . . . . . . . . . . . . . . . . .51

3.3.2.2 Preuve

52

3.3.2.3 Animation

53

3.4 Du semi-formel au formel

54

3.4.1 Principes de couplage des notations

54

3.4.2 Choix des notations

54

3.4.2.1 La possibilite de couplage avec

UM L 55

3.4.2.2 Le support d'outils disponibles pour les activites de

V&V 56

3.4.2.3 L'adequation du langage par rapport au domaine d'appli-

cation ferroviaire 57

3.4.2.4 Synthese

58

3.4.3 Approches de couplage

UML B 59

3.4.4 Discussion

60

3.5 Unied Modeling Language (UML)

60

3.5.1 Denition et Semantique

UML 61

3.5.2 Vues et diagrammes

UML 62

3.6 La methode B

64

3.6.1 Historique

64

3.6.2 Fondements et notations

65

3.6.2.1 Notation mathematique

65

3.6.2.2 Notation des machines abstraites

66

3.6.2.3 Notation de substitutions generalisees

67

3.6.3 Ranement

68

Table des matieres v

3.6.4 Modularite en

B 68

3.6.5 Obligations de preuve

69

3.6.6 Outils existants de la methode B

70

3.7 Notre approche

UML B 71

3.7.1 Motivation et cadre du projet

PERFECT

71

3.7.2 Cycle de developpement

73

3.8 Synthese

74

II CONTRIBUTIONS : DE LA S

ECURITE DES SYSTEMES D'IN-

FORMATION VERS LA S

ECURITE FERROVIAIRE75

4 Approche basee sur Role Based Access Control (RBAC)

77

4.1 Introduction

78

4.2 De la securite des SI vers la securite ferroviaire

79

4.2.1 Regles d'exploitation ferroviaires

79

4.2.2 Le modele

RBA C 83

4.2.3 SecureUML

85

4.2.4 B4MSecure

86

4.2.5 Discussion

88
4.3 Etude de cas. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

4.3.1 Scenario nominal d'autorisation de mouvement (

MA 89

4.3.2 Scenario exceptionnel

Override EOA. . . . . . . . . . . . . . .90

4.4 Modelisation

92

4.4.1 Modele fonctionnel

93

4.4.2 Politique de securite

93

4.5 Transformation en specications

B 94

4.6 Verication et validation des modeles formels

97

4.6.1Atelier BetProB. . . . . . . . . . . . . . . . . . . . . . . . . . . .97

4.6.2 Validation formelle

98

4.7 Synthese

101

4.8 Conclusion

102

5 Approche basee sur Organization Based Access Control (Or-Bac) : Ex-

tension de RBA C 103

5.1 Introduction

104
5.2

Or-Bac

vs RBA C 104

5.2.1 Le modele

Or-Bac

104

5.2.2 Les limitations du modele

RBA C 106

5.3 L'application d'

Or-Bac

sur les syst emesferro viaires 107

5.3.1 Motivation

107
vi Table des matieres

5.3.2 Le contexte

108

5.3.3 La hierarchie des organisations

109

5.3.4 Scenario

Override EOAenOr-Bac . . . . . . . . . . . . . . . . . 110

5.4 Notre vision en vue de l'interoperabilite

111

5.5 Modelisation

UML 112

5.5.1 Meta-modele

Or-Bac

etendu 112

5.5.2 Prol

UML p our

Or-Bac

114

5.5.3 Classication des organisations

115

5.6 Formalisations en

B 117

5.6.1 Architecture en

B 117

5.6.2 Calcul des permissions des dierentes organisations

119

5.7 Exemple de scenario d'accident deSaint-Romain-en-Gier. . . . . . . . . .123

5.7.1 Presentation du scenario

124

5.7.2 Analyse du comportement du systeme et raisonnement de securite

125

5.7.2.1 La demande d'interception de voie (DIV)

125

5.7.2.2 La protection de chantier

126

5.7.2.3 Installation permanente de contre sens (IPCS)

126

5.7.3 Discussion

126

5.8 Conclusion

127

6 CONCLUSION ET PERSPECTIVES

129
quotesdbs_dbs43.pdfusesText_43

[PDF] uml 2 pour les bases de données pdf

[PDF] passage du mcd au modèle relationnel

[PDF] règle typographique espace

[PDF] règle de hund pauli et klechkowski

[PDF] configuration electronique cours pdf

[PDF] manuel des procédures de sécurité informatique

[PDF] sécurité poste de travail informatique

[PDF] procédure de sauvegarde informatique pdf

[PDF] procédure de sauvegarde des données informatiques

[PDF] procedure informatique entreprise

[PDF] manuel de procédures informatiques itil

[PDF] procédure informatique exemple

[PDF] règles de vie au collège

[PDF] quelles sont les règles de vie en société

[PDF] la vie en collectivité en institution