分布式系统的分层形式化描述方法

Hierarchical formal description of distributed system

为了在开发分布式系统的过程中帮助设计者优化和验证系统,提出一种基于层次结构图形化描述方法,利用精确的数学模型描述其分布与并发行为:嵌入离散事件(DE)模型的有限自动机模型(FSM)描述软件模块内各进程间的并发及状态转换,定义基于层次图的双外推(DPO)变换建模系统拓扑结构的迁移。格件系统的描述表明该分层描述方法有效地刻画了分布式系统的并发和分布特性,为分布式系统开发提供了新的设计框架和可视化模拟方法。

In order to help designers to optimize and prove the distributed system in developing process,this paper proposed a new formal description method based on hierarchical graph. This method used precise mathematical models to describe the distribution and concurrent behaviors. It not only took advantage of embedded finite state machine to model concurrency and state transitions between processes,but also defined double push out transform to model transitions of hierarchical topology. The description of Gridjack system indicates that the hierarchical description method effectively portrays concurrent and distribution characteristics of distributed systems and provides a new design framework and simulation methods for the development of distributed systems.