| Titre : | Spécification et vérification d'un Système mobile |
| Auteurs : | Yassine Bida, Auteur ; Amira Mohammedi, Directeur de thèse |
| Type de document : | Monographie imprimée |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2018 |
| Format : | 1 vol. (70 p.) / 30 cm |
| Langues: | Français |
| Résumé : |
Les systèmes mobiles sont des systèmes ou les entités, qui les composent, peuvent changer de localité durant leurs existences. Nous avons étudie e la spécification et la verification formelles de migration et de la communication dans un réseau mobiles. Le Régulateur de vitesse adaptatif (adaptatif Cruise control ACC) est utilisé pour maintenir la vitesse d’un véhicule dans un intervalle prédéfini. Nous nous somme bas ́e sur les travaux présent ́es dans (G. Cio-banu et.RUSU)[37].qui fournissent des spécifications incomplètes. Nous avons complète les spécifications système(ACC) en utilisant l’algèbre de processus π - calcul basée sur la mobilité de lien .Puis nous avons expérimente la vérification de certaine propriétés. Nous avons présent ́e des diagrammes de séquence, la sémantique formelle, quelques propriétés, vérification par l’analyse de Mobility Workbench.Mobility Workbench [12] est utilisé comme un outil logiciel pour la vérification. |
| Sommaire : |
Contents List of tables List of figures Introduction Général L’état de l’art Systèmes mobiles et agent mobiles Introduction . . . . . . . . .. . . . . . . . . . . Systèmes mobiles . . . . . . Type de mobilité Mobilité physique : . Code mobile : . . . . Agent mobile : . . . Architecture de systèmes mobiles . . . . . . . . . . . . . . . . . . . . . . . . Composants de ressource des éléments . . . . . . . . . . . . . . . . . Composants informatiques(processus, fil) . . . . . . . . . . . . . . . . Interactions . . . . . Sites . . . . . . . . . Environnement d’exécution . . . . . . . . . . . . . . . . . . . . . . . Structures organisationnelles . . . . . . . . . . . . . . . . . . . . . . . . . . . Evaluation distante . Code `a la demande . Agent mobile . . . . pourquoi la mobilité ́e ? . . . . . . . . . . . . . . . . . . . . . . . . . . . Limites des systèmes mobile . . . . . . . . . . . . . . . . . . . . . . . . . . . Conclusion . . . . . . . . . . Formalismes pour les Systèmes Mobiles Introduction . . . . . . . . . Méthodes formelles . Pour quoi utiliser ? . Limites et inconvénients des m ́méthodes formelles . . . . . . . . . . . . Algèbres de processus . . . Algèbre de processus `a synchronisation multiple : LOTOS . . . . . . Algèbre CCS pour les processus communiquant . . . . . . . . . . . . calcul Syntaxe calcul Noms dans le-calcul . . . . . . . . . . . . . . . . . . . . . . . . . . Exemples d’interactions entre processus . . . . . . . . . . . . . . . . . Sémantique . . . . . Extensions du π calcul . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . Bisimilarit ́e forte et équivalence . . . . . . . . . . . . . . . . . . . . . Propriétés ́es modèles et ́équivalences . . . . . . . . . . . . . . . . . . . Model-checking . . . . . . . Limites . . . . . . . . Conclusion . . . . . . . . . . Spécification et vérification système ACC Régulateur de vitesse adaptatif . . . . . . . . . . . . . . . . . . . . . . . . . Avantages ACC . . . Fonctionnement . . . Dans quelles circonstances le régulateur de vitesse adaptatif r eagit-il ? Limitations . . . . . Schéma Générale . . . Schéma Fonctionnel du système ACC . . . . . . . . . . . . . . . . . . Diagramme de séquence général . . . . . . . . . . . . . . . . . . . Spécification `a l’aide du π Calcul . . . . . . . . . . . . . . . . . . . . . . . . Spécification des agents du système . . . . . . . . . . . . . . . . . . . propriétés . . . . . . Mobilité Workbench (MWB) . . . . . . . . . . . . . . . . . . . . . . . . . . Syntaxe du script MWB . . . . . . . . . . . . . . . . . . . . . . . . . spécification MWB . . . . . Verification . . . . . . . . . Step Agents Blocages Agents (deadlocks Agents) Equivalence Agent(eq) . . . . . . . . . . . . . . . . . . . . . . . . . . Bisimulation ouvert faible Agent système Acc(weq) . . . . . . . . . . Taille agent ACC(size) . . . . . . . . . . . . . . . . . . . . . . . . . . Propriétés ́es . . . . . . 3.6 Conclusion . . . . . . . . . . Conclusion Générale |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| MINF/352 | Mémoire master | bibliothèque sciences exactes | Consultable |
