The Internet has grown substantially in recent years，and an increasing number of applications are now being developed to exploit this distributed infrastructure.Mobility is an important paradigm for such applications.However，mobile distributed applications are becoming extremely complex and notoriously error-prone，thus are often difficult，inefficient and time-consuming to develop since not only do they involve complex parallel interactions between multiple components，but they must also satisfy strict requirements for correctness，reliability and security. Formal method，which has a mathematical underpinning，can provide solid foundations for describing and analyzing systems thus is widely considered as a feasible and important approach to reduce design errors and increase system reliability.It meets the requirement of understanding and reasoningabout mobile distributed computation in a rigorous manner through the use of anappropriate model.A promising approach to model mobile computation is to develop a suitable calculus.Calculi can be thought of as very simple programming languages，which provide a concise description of computation that facilitates rigorous analysis. In this thesis，two representative calculi for mobility and their variants are studied.They are mainly the π-Calculus which reduces the concept of mobility to reference mobility and the Calculus of Mobile Ambient adopting explicitcode or agent mobility.The π-calculus is an inheritance and development of CCS，which allows processes to exchange specific values-channel names,thus are capable of expressing systems that can dynamically reorganize their communication topology during their evolution while the Calculus of Mobile Ambient includes the notion of locations and Drimitives for moving processes，thus can explicitlymodel the notion of mobility.Both of them provide a conceptual framework for understanding mobility and mathematical tools for expressing mobile distributed systems and reasoning about their behaviors. Based on them，we have investigated various issues on modelling，specifying，verifying and implementing mobile distributed systems.In details，we perform a systematic and deep study of the semantic theory，in terms of bisimulation equivalence，axiomatization systems，modal and temporal logic and verification algorithms.Moreover，we exploit two applications of mobile process calculi，that is，semi-structured data modelling andsystem performance analysis.The following are major contribntions:·We settle the problem of axiomatizing open barbed bisimilation on π-calculus.Based on a tractable characterization of this equivalence，called quasi-open bisimilarity，we give axiomatization systems for strong and weak quasi-open bisimulation，thus for open barbed congruence.Such systems are provided in two styles,one usesequalities indexed by finite name set，the other uses a special schematic law to deal with restriction.The axiomatic system for weak open barbed congruence is obtained by adding some tau laws to the axiomatic system for the strong case.The soundness and completeness of these systems are shown.·We study the symbolic semantics of the weak open congruences on finite π processes with the mismatch operator.The standard definition of weak open congruence gives rise to an ill-defined equivalence in the presence of the mismatch operator.