Web Service composition Model-Cheking

الموضوعات

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

الملخص

Analyzing and verifying a complex web service composition permits giving answers about their correctness, reliability and safety. Indeed, (Model-Checking: "check on the model"), is a very well known method to verify the qualitative (e.g.: state accessibility, liveness, blocking, etc...) as well as the quantitative properties (e.g.: response time) on the model. The Petri net formalism and its extensions are widely used in the literature for their important number of advantages as: (graphical and intuitive representations, abundant analysis techniques...etc.). We are interested in the Petri net formalism as a modelling tool, extended to time constraints. Because of the infinite state space of the model, many standard methods for the state space abstraction are used, gathering a set of states sharing some properties and based on the State Class formalism. (TINA: "TIme Network Analyzer") is one of the most known tools for this end. Finally, analysing and verifying qualitative and quantitative properties on the model as well as on the system itself became possible.

روابط وملفات

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

رقم الوثيقة

ff90bf9e-3a90-45a6-9be2-8105bae5d051

رقم العقد

0

نوع الوسائط

Crawler

نوع المحتوى

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

صيغة المصدر

ماستر (LMD)

نوع الملف

pdf text

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

954110_1.pdf

بيانات النشر

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

[{"name_ar":" Abdia Hamdani","title_ar":"اشراف","title_en":"Supervision"},{"name_ar":" Rosa Rebouh","title_ar":"اعداد","title_en":"Preparation"}]

اللغة

English

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

اسم المصدر

Web Service composition Model-Cheking

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

عدد الصفحات

0

ترجمة الملخص

L’analyse et la vérification de la composition des services web permettent de répondre aux questions liées, essentiellement, à la fiabilité et à la sûreté de fonctionnement de ces derniers. En effet, (le Model-Checking : "vérification du/sur le modèle"), est une méthode très connue permettant de vérifier les propriétés qualitatives (e.g : accessibilité d’un état, vivacité, blocage, etc...) et/ou quantitatives (e.g : la réponse du temps borné) sur le modèle. Le formalisme des réseaux de Petri et ses extensions sont largement utilisés dans la littérature, offrant un nombre considérable d’avantages citons : (sa représentation graphique et intuitive, ses techniques abondantes d’analyses...etc.). Nous nous intéressons aux réseaux de Petri comme outil de modélisation, étendu au temps. Cependant, l’espace d’états est généralement infini et de nombreuses méthodes sont utilisées pour l’abstraction de l’espace d’états du modèle ceci consiste à regrouper un ensemble d’états partageant les mêmes propriétés basé sur le formalisme de classe d’états. (TINA : "TIme Network Analyzer") est l’un des outils les plus connus pour cela. Enfin, l’analyse et la vérification des propriétés qualitatives et quantitatives sur le modèle, et bien évidemment, sur le système en question deviennent possibles.

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

Model checking, Timed Petri nets, Web service composition, State space, Verification tools, Quantitative and qualitative properties.

إشراف وإعداد

الإشراف

Abdia Hamdani

الإعداد

Rosa Rebouh

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