Vers une démarche efficace de traitement du model Checking dans les Cloud Computing

ALLAL Lamia

Type de document Thèse
Langue fre
Titre Vers une démarche efficace de traitement du model Checking dans les Cloud Computing [ressource textuelle manuscrite]
Auteur(s) ALLAL Lamia (Auteur)
G. BELALEM (Directeur de thèse)
P. DHAUSSY (Directeur de thèse)
Adresse bib. Université Oran 1 : université oran 1,2018
Collation XII-76F. ; 30CM. + CD.
Notes RESUME EN FRANCAIS ET EN ANGLAIS. BIBLIOG.71-76F.
Notes de thèse Doctorat sciences : Informatique : ORAN 1 : 2018
Numéro TH4862
Theme Informatique
Mot (s) clé model checking
vérification formelle
Exploration
Algorithmes parallèles
Temps d'exécution
algorithmes distribués
Espace mémoire
Spin
Gain en temps
Structures de données
Résumé Le Model checking a longtemps été utilisé comme moyen de vérification des spécifications formelles. C'est une technique de vérification qui explore tous les états possibles du système. Cette technique détermine si un système donné satisfait sa spécification. Cette technique souffre du problème d'explosion en temps et en espace mémoire. Dans cette thèse, nous avons proposé d'exploiter les ressources machines afin d'augmenter le gain en temps d'exécution en utilisant des algorithmes parallèles. Nous avons réalisé une comparaison entre deux approches parallèles et nous avons montré que notre approche était plus avantageuse en temps d'exploration et en espace mémoire nécessaire pour le stockage des états. Nous avons par la suite effectué une comparaison entre une exploration parallèle et une exploration distribuée, nous avons conclu par une étude expérimentale, que l'approche parallèle affichait de meilleurs résultats et que le choix des structures de données était très important pour diminuer la complexité spatiale et temporelle d'un algorithme.

ALLAL Lamia
Vers une démarche efficace de traitement du model Checking dans les Cloud Computing [ressource textuelle manuscrite] / ALLAL Lamia; Dir. G. BELALEM, Dir. P. DHAUSSY.-Université Oran 1 : université oran 1,2018.-XII-76F. ; 30CM. + CD.
- RESUME EN FRANCAIS ET EN ANGLAIS. BIBLIOG.71-76F.
Doctorat sciences : Informatique : ORAN 1 : 2018
.
Numéro normalisé TH4862

model checking
vérification formelle
Exploration
Algorithmes parallèles
Temps d'exécution
algorithmes distribués
Espace mémoire
Spin
Gain en temps
Structures de données

Le Model checking a longtemps été utilisé comme moyen de vérification des spécifications formelles. C'est une technique de vérification qui explore tous les états possibles du système. Cette technique détermine si un système donné satisfait sa spécification. Cette technique souffre du problème d'explosion en temps et en espace mémoire. Dans cette thèse, nous avons proposé d'exploiter les ressources machines afin d'augmenter le gain en temps d'exécution en utilisant des algorithmes parallèles. Nous avons réalisé une comparaison entre deux approches parallèles et nous avons montré que notre approche était plus avantageuse en temps d'exploration et en espace mémoire nécessaire pour le stockage des états. Nous avons par la suite effectué une comparaison entre une exploration parallèle et une exploration distribuée, nous avons conclu par une étude expérimentale, que l'approche parallèle affichait de meilleurs résultats et que le choix des structures de données était très important pour diminuer la complexité spatiale et temporelle d'un algorithme.

00100000000000001219430001028
018  $aTH4862
100  $a                         y50
101  $afre$cfre
2001 $aVers une démarche efficace de traitement du model Checking dans les Cloud Computing$bressource textuelle manuscrite
210  $aUniversité  Oran 1$cuniversité oran 1$d2018
215  $aXII-76F.$d30CM.$eCD.
300  $aRESUME EN FRANCAIS ET EN ANGLAIS. BIBLIOG.71-76F.
328 1$bDoctorat sciences $cInformatique$eORAN 1$d2018
330  $aLe Model checking a longtemps été utilisé comme moyen de vérification des spécifications formelles. C'est une technique de vérification qui explore tous les états possibles du système. Cette technique détermine si un système donné satisfait sa spécification. Cette technique souffre du problème d'explosion en temps et en espace mémoire. Dans cette thèse, nous avons proposé d'exploiter les ressources machines afin d'augmenter le gain en temps d'exécution en utilisant des algorithmes parallèles. Nous avons réalisé une comparaison entre deux approches parallèles et nous avons montré que notre approche était plus avantageuse en temps d'exploration et en espace mémoire nécessaire pour le stockage des états. Nous avons par la suite effectué une comparaison entre une exploration parallèle et une exploration distribuée, nous avons conclu par une étude expérimentale, que l'approche parallèle affichait de meilleurs résultats et que le choix des structures de données était très important pour diminuer la complexité spatiale et temporelle d'un algorithme.
600  $aExploration
602  $avérification formelle
602  $aalgorithmes distribués
605  $amodel checking
605  $aTemps d'exécution
605  $aEspace mémoire
605  $aGain en temps
605  $aStructures de données
606  $aAlgorithmes parallèles
606  $aSpin
615  $n22$aInformatique$2theme CCDZ CERIST 2011
700  $aALLAL Lamia$4070
701  $aG$b BELALEM$4727
701  $aP$b DHAUSSY$4727
801 0$aDZ$bCCDZ CERIST
801 1$aDZ$bCCDZ CERIST
801 2$aDZ$bCCDZ CERIST
801 3$aDZ$bCCDZ CERIST
901$ac

Type de document	Thèse
Langue	fre
Titre	Vers une démarche efficace de traitement du model Checking dans les Cloud Computing [ressource textuelle manuscrite]
Auteur(s)	ALLAL Lamia (Auteur) G. BELALEM (Directeur de thèse) P. DHAUSSY (Directeur de thèse)
Adresse bib.	Université Oran 1 : université oran 1,2018
Collation	XII-76F. ; 30CM. + CD.
Notes	RESUME EN FRANCAIS ET EN ANGLAIS. BIBLIOG.71-76F.
Notes de thèse	Doctorat sciences : Informatique : ORAN 1 : 2018
Numéro	TH4862
Theme	Informatique
Mot (s) clé	model checking vérification formelle Exploration Algorithmes parallèles Temps d'exécution algorithmes distribués Espace mémoire Spin Gain en temps Structures de données
Résumé	Le Model checking a longtemps été utilisé comme moyen de vérification des spécifications formelles. C'est une technique de vérification qui explore tous les états possibles du système. Cette technique détermine si un système donné satisfait sa spécification. Cette technique souffre du problème d'explosion en temps et en espace mémoire. Dans cette thèse, nous avons proposé d'exploiter les ressources machines afin d'augmenter le gain en temps d'exécution en utilisant des algorithmes parallèles. Nous avons réalisé une comparaison entre deux approches parallèles et nous avons montré que notre approche était plus avantageuse en temps d'exploration et en espace mémoire nécessaire pour le stockage des états. Nous avons par la suite effectué une comparaison entre une exploration parallèle et une exploration distribuée, nous avons conclu par une étude expérimentale, que l'approche parallèle affichait de meilleurs résultats et que le choix des structures de données était très important pour diminuer la complexité spatiale et temporelle d'un algorithme.