异步通信系统的合理性检测
Soundness checking of asynchronous communication systems
王帅 1代飞 1黄苾 1莫启 2付晓东3
作者信息
- 1. 西南林业大学大数据与智能工程学院,云南 昆明 650224
- 2. 云南大学软件学院,云南 昆明 650091
- 3. 昆明理工大学信息工程与自动化学院,云南 昆明 650500
- 折叠
摘要
异步通信系统是一种并发分布式系统,由一组具有无界缓冲区的分布式组件通过异步通信构成.分析异步通信系统的核心问题是检测其合理性,即确保组成系统的分布式组件可以无错误地进行异步通信.然而,基于无界缓冲区的异步通信容易导致异步通信系统产生无穷状态空间,从而使得对无穷状态空间进行穷举分析是不可判定的.鉴于此,提出一种异步通信系统的合理性检测方法,用于分析具有无界缓冲区异步通信系统的合理性.首先,使用标号迁移系统建模分布式组件,并使用异步组合定义基于分布式组件的异步通信系统;其次,根据异步通信系统的特征,提出了三种合理性定义;然后,基于稳定性性质,提出了检测具有无界缓冲区异步通信系统合理性的充分条件;最后,使用进程分析工具实现了所提方法,实验结果表明了所提方法的有效性.
Abstract
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 un-bounded buffers easily leads to an infinite state space for asynchronous communication systems,which makes it un-decidable to exhaustively analyze the infinite state space.A soundness checking method for asynchronous communi-cation 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 com-position 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 tool-kit,and its effectiveness was verified with the experiment.
关键词
异步通信系统/无界缓冲区/合理性/稳定性/标号迁移系统Key words
asynchronous communication system/unbounded buffers/soundness/stability/labelled transition systems引用本文复制引用
基金项目
国家自然科学基金资助项目(61862065)
国家自然科学基金资助项目(62262063)
云南省重点研发项目(202402AD080002-5)
云南省基础研究面上项目(202001BB050031)
云南省软件工程重点实验室开放基金青年项目(2020SE401)
云南省窦万春专家工作站资助项目(202105AF150013)
云南省"兴滇英才支持计划"产业创新人才资助项目(XDYC-CYCX-2022-0009)
云南省科协青年科技人才托举工程资助项目()
出版年
2024
NETL
NSTL
万方数据