Plusieurs analyses ont été proposées pour garantir ou prouver des propriétés sur les systèmes mobiles. Elles considèrent essentiellement des propriétés de sûreté (<<safety properties>>), comme la confidentialité de l'information qui circule dans les systèmes de communication ou comme le nombre de processus qui sont utilisés par les systèmes.
Des analyses par typage [9] ou par analyse du flux de communication [1] permettent de garantir que les échanges d'informations entre les agents d'un réseau ne violent pas les droits d'accès défini par le concepteur du réseau. Cependant, dans ces deux analyses, le concepteur ne peut donner des droits différents à des processus créés récursivement par un même serveur. Dans le cas d'un protocole client-serveur, ces analyses permettront de prouver que l'information des clients ne peut être seulement transmise qu'au serveur et aux clients, mais elles ne peuvent montrer que l'information d'un client n'est transmise qu'au serveur et à lui-même. Récemment, un nouveau système de typage a été proposé [3] pour pallier à ce problème. Néanmoins, il ne peut permettre de prouver la non-interférence entre deux instances récursives d'un même serveur que lorsque celles-ci restent confinées dans le serveur. Ce n'est pas le cas dans une autre analyse [13] qui se restreint aux systèmes dont les ressources ne sont pas imbriquées.
Les analyses du nombre des processus [8,12] ne sont pas assez précises: elles ne permettent de répondre ni au problème de l'exclusion mutuelle, ni à celui de la détection des exhaustions de ressources. De plus, leur coût est exponentiel du fait de l'explosion combinatoire.
Enfin, récemment a été proposée une analyse par système de types [10] qui permet de garantir qu'un système ne sera jamais bloqué. Il s'agit là encore d'une propriété de sûreté. Cependant, la réponse à ce problème est très partielle et beaucoup trop de systèmes sans blocages ne sont pas typables.