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 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.