Combining Mobility with State

摘要

Our work is motivated by practice in Peer-to-Peer networks and Object-Oriented systems where instantiation and dynamically reconfigurable interconnection are essential paradigms. For example, in a Peer-to-Peer network nodes can exchange data to complete tasks. Nodes can leave or join the network at any time. In Object-Oriented systems, an object can be uniquely identified and will communicate with other objects. In this paper we outline a formal framework which supports this kind of interaction so that the integrity of each active object or node is preserved, and so that we can reason about the overall behaviour of the system. The formal framework is based on a combination of the π-calculus and the B-Method.