Specification, analysis and prototyping of mobile code systems.

In the past few years dynamic and recongurable systems have evolved and new strategy and paradigms for the development of applications have been devised. In this thesis we study mobile code based systems focusing on the importance of formalization and investigation of the potential of code mobility. Mobile code paradigms have been used in dierent systems, however, as most of these are Java based, the potential of code mobility are some-how lost behind the Java language capabilities, and design choices related to mobility have been conditioned by implementation choices. In this thesis we reason on code mobility systems at the design level in order to investigate novel powerful approaches. This thesis is composed of dierent parts. We rst introduce a coordination based language and a model checker to reason on formalization of mobile code based systems with automatic analysis. Properties of mobile agents, of their interaction and behavior may be formally expressed and veried against the system specication. Then, in order to express code mobility potential and to formalize the basic constructs for code migration, we describe a formal language for the specication of very ne-grained mobility. Every line of code, and every variable declaration can be mobile, giving a very high exibility in the range of application. A prototype of this model implemented in Java is also presented to validate the implementability of the model. Finally, we show a possible incarnation of the ne-grained mobility approach based on XML. The approach allows XML documents to be updated cutting, extending, or replacing parts of the tree structure of the document. We exploit this idea to incrementally update remote code. The approach can be used in dierent domains; we describe possible applications in graphic user interface management, document consistency checking and management of application on thin clients like personal digital assistants (PDAs).