Distributed programs are complex and hard to reason about. An important source of difficulty in actual installed distribution systems is their open-ended nature; unlike modules described in traditional programming languages, over time distributed components may be added or removed, and they may change their connectivity. The goal of this project is to study how large systems can be divided into extensible modular components about which one can reason separately. Such a separation will facilitate the development and incremental modification of code. The research is based on a model of Actors: The model supports data encapsulation, procedural abstraction, asynchronous communication, reconfigurability, and dynamic creation. A formal algebra of actor configurations will be developed and methods for composing properties of open actor systems will be studied. The proposed research will provide a foundation for the formal verification of safety-critical distributed software systems.
