R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, I, Information and Computation, vol.100, issue.1, pp.1-77, 1992.
DOI : 10.1016/0890-5401(92)90008-4

L. Cardelli and A. Gordon, Mobile ambients, Theoretical Computer Science, vol.240, issue.1, pp.177-213, 2000.
DOI : 10.1016/S0304-3975(99)00231-5

C. Fournet and G. Gonthier, The reflexive chemical abstract machine and the Join-calculus, Proceedings of the 23rd ACM Symposium on Principles of Programming Languages, pp.372-385, 1996.

R. D. Nicola, G. Ferrari, and R. Pugliese, KLAIM: a kernel language for agents interaction and mobility, IEEE Transactions on Software Engineering, vol.24, issue.5, pp.315-330, 1998.
DOI : 10.1109/32.685256

J. Vitek and G. Castagna, Seal: A Framework for Secure Mobile Computations, ICCL Workshop: Internet Programming Languages, pp.47-77, 1998.
DOI : 10.1007/3-540-47959-7_3

L. Cardelli and A. Gordon, Anytime, anywhere. Modal logics for mobile ambients, Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pp.365-377, 2000.
DOI : 10.1145/325694.325742

L. Caires and L. Cardelli, A spatial logic for concurrency (part I), Information and Computation, vol.186, issue.2, pp.194-235, 2003.
DOI : 10.1016/S0890-5401(03)00137-8

R. D. Nicola, M. Loreti, and . Klaim, A Modal Logic for Klaim, Proc. Algebraic Methodology and Software Technology, pp.339-354, 2000.
DOI : 10.1007/3-540-45499-3_25

D. Sangiorgi, Extensionality and intensionality of the ambient logic, Proc. of the 28th Intl. Conf. on Principles of Programming Languages (POPL'01), pp.4-17, 2001.

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

H. Baumeister, N. Koch, P. Kosiuczenko, P. Stevens, and M. Wirsing, UML for Global Computing, Global Computing, pp.1-24, 2003.
DOI : 10.1007/978-3-540-40042-4_1

H. Baumeister, N. Koch, P. Kosiuczenko, and M. Wirsing, Extending Activity Diagrams to Model Mobile Systems, Objects, Components, Architectures, Services, and Applications for a Networked World, pp.278-293, 2002.
DOI : 10.1007/3-540-36557-5_21

M. Object and . Group, UML 2.0 Superstructure Specification, Final Adopted Specification ptc/03-08-02, 2003.

S. Merz, A more complete TLA, FM'99: World Congress on Formal Methods, pp.1226-1244, 1999.
DOI : 10.1007/3-540-48118-4_15

G. Ostertag, Definite Descriptions: A Reader, 1998.

L. Lamport, How to write a long formula, Digital Equipment Corporation, 1993.
DOI : 10.1007/BF01211870

J. Zappe, Towards a mobile TLA, 2005.

M. Abadi and S. Merz, On TLA as a logic Deductive Program Design, NATO ASI series F, pp.235-272, 1996.

J. Abrial, The B-Book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

M. Büchi and E. Sekerinski, A foundation for refining concurrent objects, Fundamenta Informaticae, vol.44, issue.1 2, pp.25-61, 2000.

M. Abadi and L. Lamport, The existence of refinement mappings, Theoretical Computer Science, vol.82, issue.2, pp.253-284, 1991.
DOI : 10.1016/0304-3975(91)90224-P

S. Meng, Z. Naixiao, and L. S. Barbosa, On Semantics and Refinement of UML Statecharts: A Coalgebraic View, Proc. 2 nd IEEE Int. Conf. Software Engineering and Formal Methods, pp.164-173, 2004.