To My beloved family … To my true friends …

AKNOWLEDGMENT

Firstly, I would like to thank my supervisor Professor Mohammed Mostefai for providing me with supervision, motivation and encouragement throughout the course of my work. Without his

care, and friendship, I would not be able to complete this work. In particular I would to express to him my gratitude for his active andconstructive

participation in this thesis.

I would like to thank Professor Benouattass Nourredine from department of physics for his invaluable and precious help in this work.

I would to thank also all my family members for their help, support and encouragement.

ABSTRACT

This doctoral thesis is part of the research activities of the Laboratory of Automatic of Sétif (L.A.S). It treatsspecification and verification of production systems in general and mobile enterprises in particular. The major contribution of this thesis appears in the study of the integration of mobility in the enterprises. Indeed, an architecture for mobile enterprises is proposed and comprises a Web-Services layer and a multi-agents layer combining static agents and mobile agents. This contribution is organized intwo phases: the first phase concerns the modelling of workflow based enterprises. The model is validated analytically by a performance analysis. The second phase consists to explore and exploit some formal tools for the specification of the mobile enterprises: Two formalisms are retained the REACTNets for the Web-Services layer and MAUDE for the

behaviour of the mobile agents.

RÉSUMÉ

Letravail de cette thèse s’inscrit dans le cadre des activités de recherche du Laboratoire d’Automatique de l’Université de Sétif (L.A.S). Il traite de la spécification et de la vérification des systèmes de production « entreprises » en général et des entreprises mobiles en particulier. La contribution majeure de cette thèse apparaît dans l’étude de l’intégration de la mobilité dans les entreprises.En effet, une architecture des entreprises mobiles est proposée et comporte une couche WebServices et une couche multi-agents combinant des agents statiques et des agents mobiles. Cette contribution est organisée en deux phases : la première traite de la modélisation des entreprises moyennant les WorkFlow. Le modèle étant validé analytiquement par une analyse de performances. La seconde consiste àexplorer et exploiter quelques outils formels pour la spécification des entreprises mobiles à savoir : les REACTNets pour la spécification et la vérification de la couche Web-Services et MAUDE pour la spécification et la vérification du comportement des agents mobiles.

????????????????

??? ??? ??? ????? ?? ?? ??? ???? ???? ???? ?????

???? ?? ??

?? ? ? ?? ?? ?? ??? ??? ?? ??

??? ??? ?? ? ?? ??? ?. ?? ??

?? ? ??? ? ?? ??? ?? ??? ??? ??? ? ?? ?? ?? ???? ?? ????? ?? ? ??? ?.? ??? ??? ?? ??? ???? ???? ?? ?? ??? ??? ???? ??? ???? ??? ??? ??? ? ?? ?.? ???

??? ?? ? ? ? ? ?? ??? ? ??

?? ? ) ? (L.A.S???

?? ? ? ????

?? ?? ??

?? ??? ? ????

?? ? ? ? ? ) ? (Web-Services?? ?? ?? ) ? ( Systèmes multi-agents?? ?? ??:? ??? ??? ???? ??? ?? ??? ?? ??? ?? ??? ??.?

?? ?????? ??? ???

?? ? ? ??

?? ) ??( WorkFlow??

?? ????? ? ? ? ? ?? ?? ? ?? ?? ? ??? ?.? ???? ??? ???

???

?????

???

?? ? ? ??? ?? ??

?? ?? ? ? )? ( ECATNets?? ? ?? ?? MAUDE?? ? ??

?? ? ??? ? ??

PUBLICATIONS RELATED TO THIS THESIS
Conferences (1) Faiza Bouchoul -Mohammed Mostefai-Zohour Kaddem « Towards M-Manufacturing – Case Study : a Fault Tolerant Model for
ThM-Maintenance of Spare Parts with Mobile Agents » IEEE : 4 Conference: Sciences of Electronic, Technologies of

International And

Information

Telecommunications) – SETIT 07 – Hamamet marsh 25-29 2007 Tunisia (2) Faiza Bouchoul – Mohammed Mostefai « MOBIFLEX a generic architecture for healthcare systems » IEEE : First International conference on emedical systems E-Medisys 07 – FEZ october 24-26…