Spécification et vérification d’un Système mobile

Abstract

Les syst`emes mobiles sont des syst`emes o`u les entit´es, qui les composent, peuvent changer de localit´e durant leurs existences. Nous avons ´etudi´e la sp´ecification et la v´erification formelles de migration et de la communication dans un r´eseau mobiles.Le R´egulateur de vitesse adaptatif(adaptatif cruise control ACC) est utilis´e pour maintenir la vitesse d’un v´ehicule dans un intervalle pr´ed´efini.Nous nous somme bas´e sur les travaux pr´esent´es dans (G. Ciobanu et.RUSU)[37].qui fournissent des sp´ecifications incompl`etes.Nous avons compl´et´e les sp´ecifications syst`eme(ACC) en utilisant l’alg`ebre de processus π-calcul bas´ee sur la mobilit´e de lien .Puis nous avons exp´eriment´e la v´erification de certaine propri´et´es. Nous avons pr´esent´e des diagrammes de s´equence,la s´emantique formelle,quelques propri´et´es, v´erification par l’analyse de Mobility Workbench.Mobility Workbench [12] est utilis´e comme un outil logiciel pour la v´erification