Collaborative Research: Reasoning About Open Systems

点击翻译按钮获取中文摘要

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 can 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 is being developed and methods for composing properties of open actor systems is studied. The research seeks a foundation for the formal verification of safety-critical distributed software systems.