| The Internet is increasingly becoming an indispensable tool for our social and economic activities. The latest technologies, such as grid or peer-to-peer computing, have allowed us to take advantage of its connectivity and widely distributed computing power. We refer to the intuitive notion capturing these distributed and dynamically changing systems as Global Computing. These systems are inherently open; they can be dynamically re-configured as their computational entities are relocated or as new entities are added. Therefore, these systems must rely on run-time controls to present any inconsistencies between different entities and ensure their correct operation.; Boxed Ambients (BA) is a calculus used to describe and analyze concurrent distributed systems with mobility. BA's type system guarantees communication type safety, and its algebraic theory allows reasoning about its models. However, as most calculi for concurrency, BA assumes that the systems it describes are closed, i.e., the set of entities of those systems are fixed. Because of this assumption, BA is not rich enough to model Global Computing. This lack of expressive power motivated the work on the first part of this dissertation where we introduce a calculus called Boxed Ambients with Communication Interfaces (BACI). BACI was defined by modifying BA's operational semantics and type system to address the dynamic behavior present in Global Computing, and it develops an algebraic theory based on the new operational semantics.; A limitation of earlier ambient calculi is that each channel can only transmit information of a predetermined fixed type. However, to describe realistic scenarios, communicating parties should be able not only to exchange heterogeneous data, but also to follow a specified protocol. This limitation triggered the work on the second part of this thesis, where we introduce the calculus of Boxed Ambients with Safe Sessions (BASS). Like BACI, BASS extends BA to support Global Computing, but it also enables the specification of channels for communication protocols using sessions---i.e., series of communication exchanges between two entities. We formally show that BASS ensures communication type safety during sessions, and it guarantees that sessions are not interfered by entity relocation. |
