异步通信系统的合理性检测

Soundness checking of asynchronous communication systems

异步通信系统是一种并发分布式系统,由一组具有无界缓冲区的分布式组件通过异步通信构成。分析异步通信系统的核心问题是检测其合理性,即确保组成系统的分布式组件可以无错误地进行异步通信。然而,基于无界缓冲区的异步通信容易导致异步通信系统产生无穷状态空间,从而使得对无穷状态空间进行穷举分析是不可判定的。鉴于此,提出一种异步通信系统的合理性检测方法,用于分析具有无界缓冲区异步通信系统的合理性。首先,使用标号迁移系统建模分布式组件,并使用异步组合定义基于分布式组件的异步通信系统;其次,根据异步通信系统的特征,提出了三种合理性定义;然后,基于稳定性性质,提出了检测具有无界缓冲区异步通信系统合理性的充分条件;最后,使用进程分析工具实现了所提方法,实验结果表明了所提方法的有效性。

An asynchronous communication system is a concurrent distributed system consisting of a set of distributed components with unbounded buffers that communicate asynchronously.The core problem of analyzing asynchronous communication systems is to check their soundness,that is,to ensure that the distributed components that make up the system can communicate asynchronously without errors.However,asynchronous communication based on unbounded buffers easily leads to an infinite state space for asynchronous communication systems,which makes it undecidable to exhaustively analyze the infinite state space.A soundness checking method for asynchronous communication systems was proposed to analyze the soundness of asynchronous communication systems with unbounded buffers.The distributed components were modeled using the labeled transition systems,and the asynchronous composition was used to define the asynchronous communication system based on distributed components.According to the characteristics of the asynchronous communication system,three soundness definitions were proposed.Based on the stability properties,sufficient conditions for checking the soundness of asynchronous communication systems with unbounded buffers were proposed.Finally,the proposed method was implemented using process analysis toolkit,and its effectiveness was verified with the experiment.