Une approche de spécification et de vérification des systèmes logiciels à base d’agents mobiles en utilisant UML mobile et π-calcul

الموضوعات

علوم تطبيقية وتكنولوجية

الملخص

Les systèmes logiciels à base d'agents mobiles sont un type particulier d'applications qui bénéficient des avantages des agents mobiles. Cela conduit à un nouveau paradigme qui peut résoudre multiples problèmes complexes dans plusieurs domaines et secteurs, par exemple la gestion du réseau, le commerce électronique et le e-learning. La modélisation et analyse des systèmes logiciels à base d'agents mobiles présentent d'énormes difficultés; cela est dû à l'utilisation des agents mobiles qui génère souvent de nouvelles situations de plus en plus compliquées. Mobile UML (M-UML) a été proposé comme une extension de l’UML pour modéliser ces systèmes. π-calcul est une méthode formelle rigoureuse introduite pour spécifier le comportement des systèmes concurrents avec communications mobiles. Dans cette thèse, nous proposons les MSDs (Mobile Statechart Diagrams); Une extension des diagrammes d'états-transition M-UML qui fournissent plus d'éléments de modélisation. Ensuite, une approche intégrée MSDs / π-calcul est développée pour la modélisation et la vérification des systèmes logiciels à base d'agents mobiles en transformant le premier vers le dernier. Les spécifications π-calcul dérivées sont ensuite utilisées pour analyser et vérifier ces systèmes à l'aide des outils d'analyse du π-calcul (tel que l’outil MWB). L'approche est illustrée par une étude de cas. Nous fournissons également une implémentation de l'approche afin d'automatiser ses différentes étapes. AToM3 est utilisé comme outil de transformation.

روابط وملفات

التعريف والنوع

رقم الوثيقة

020feebf-b42e-4bc4-be9b-28bbd92decb5

رقم العقد

0

نوع الوسائط

Crawler

نوع المحتوى

الرسائل العلمية

صيغة المصدر

رسائل دكتوراة

نوع الملف

pdf text

أسماء الملفات

302467_1.pdf

بيانات النشر

ألقاب المؤلفين

[{"name_ar":"Aissam Belghiat","title_ar":"اعداد","title_en":"Preparation"},{"name_ar":"Chaoui Allaoua","title_ar":"اشراف","title_en":"Supervision"}]

اللغة

French

المصدر والدورية

اسم المصدر

Une approche de spécification et de vérification des systèmes logiciels à base d’agents mobiles en utilisant UML mobile et π-calcul

المحتوى والصفحات

عدد الصفحات

0

ترجمة الملخص

أنظمة البرمجيات القائمة على وكيل متنقل هي نوع خاص من التطبيقات التي تستفيد من ايجابيات الوكالء المتنقلون .وهذا يؤدي إلى نموذج جديد يمكن أن تحل بواسطته المشاكل المعقدة المتعددة في العديد من الميادين والمجاالت، على سبيل المثال، إدارة الشبكات، والتجارة اإللكترونية، والتعليم اإللكتروني. نمذجة وتحليل النظم والبرمجيات المستندة على الوكالء المتنقلون يولد صعوبات هائلة؛ ويرجع ذلك إلى استخدام الوكالء المتنقلون والتي غالبا ما ينتج حاالت جديدة معقدة على نحو متزايد .وقد اقترح المحمول UML-M كامتداد لـ UML لنمذجة هذه األنظمة . calculus-π هو أسلوب رسمي صارم قدم لتحديد سلوك النظم المتزامنة مع االتصاالت المتنقلة. في هذه األطروحة، نقترح Statechart Mobile (MSDs (Diagrams؛ الذي هو امتداد لمخططات Diagrams Statechart UML-M التي توفر المزيد من عناصر النمذجة. بعد ذلك نطور طريقة مركبة / MSDs calculus-π لوضع النماذج والتحقق من أنظمة البرمجيات القائمة على الوكالء المتنقلون بترجمة األول إلى الثاني. ثم يتم استخدام مواصفات -π calculus لتحليل ومراجعة هذه النظم باستخدام األدوات التحليلية لـ -π calculus) مثل أداة MWB .(نوفر دراسة حالة اليضاح الطريقة والتمكن من تطبيقها .و نقدم أيضا تطوير الطريقة من أجل اتمتت الخطوات المختلفة . 3 باستعمال اداة AToM Mobile agent-based software systems are a special type of applications which benefit from the advantages of mobile agents. This leads to a new paradigm that can solve multiple complex problems in several fields and areas, e.g. network management, electronic commerce, and e-learning. Modeling and analysis of mobile agent-based software systems would present enormous difficulties; this is due to the use of mobile agents which often generates new situations increasingly complicated. Mobile UML (M-UML) has been proposed as an extension of UML to model these systems. π-calculus is a rigorous formal method introduced to specify the behavior of concurrent systems with mobile communication. In this thesis, we propose MSDs (Mobile Statechart Diagrams); an extension of MUML statechart diagrams that provide more modeling elements. Then an integrated approach MSDs/π-calcul is developed for modeling and verification of mobile agent-based software systems by translating the former to the later. The derived π-calculus specifications are then used to analyze and check these systems using π-calculus analytical tools (such as MWB tool). The approach is illustrated by a case study. We provide also an implementation of the approach in order to automate its different steps. AToM3 is used as a transformation tool.

كلمات الباحثين

تحليل, نمذجة

إشراف وإعداد

الإشراف

Chaoui Allaoua

الإعداد

Aissam Belghiat

الاقتباسات الببليوغرافية