Framework of Performance Evaluation for Mobile Process Based on Mobile Ambient ∗

Formal methodology for distributed and concurrent system, especially computation system with mobility, is increasingly important both in the theory and the practice. Based on the Calculus of Mobile Ambi-ent (MA), a widely studied formal mechanism for mo-bile computation, this paper focuses on the quantitative analysis of mobile computation system and provides a framework of performance evaluation for it. In details, this paper introduces an enhanced labelled transition system as the system model, and assigns rate to each label through so-called cost function. Based on it, the labelled transition system can be mapped to Continuous Time Markov Chains and thus performance evaluation can be carried out by standard numerical techniques and tools. In some sense, the main work of this pa-per can be regarded as integrating behavior and perfor-mance analysis in a compositional formal framework, which provides some basis of unified formal methodol-ogy for the development of mobile system