Collaborative Research: Reasoning About Open Systems

分布式程序很复杂，很难推理。实际安装的分布式系统的一个重要困难来源是它们的开放性；与传统编程语言中描述的模块不同，随着时间的推移，分布式组件可能会被添加或删除，并且它们可能会改变它们的连接性。这个项目的目标是研究如何将大型系统划分为可扩展的模块化组件，这些组件可以单独进行推理。这种分离可以促进代码的开发和增量修改。研究基于Actors的模型：该模型支持数据封装、过程抽象、异步通信、可重构性和动态创建。开发了参与者配置的形式代数，并研究了组成开放参与者系统的属性的方法。该研究为安全关键型分布式软件系统的形式化验证奠定了基础。

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.