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

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

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

asynchronous communication systemunbounded bufferssoundnessstabilitylabelled transition systems

王帅、代飞、黄苾、莫启、付晓东

展开 >

西南林业大学大数据与智能工程学院,云南 昆明 650224

云南大学软件学院,云南 昆明 650091

昆明理工大学信息工程与自动化学院,云南 昆明 650500

异步通信系统 无界缓冲区 合理性 稳定性 标号迁移系统

国家自然科学基金资助项目国家自然科学基金资助项目云南省重点研发项目云南省基础研究面上项目云南省软件工程重点实验室开放基金青年项目云南省窦万春专家工作站资助项目云南省"兴滇英才支持计划"产业创新人才资助项目云南省科协青年科技人才托举工程资助项目

6186206562262063202402AD080002-5202001BB0500312020SE401202105AF150013XDYC-CYCX-2022-0009

2024

10.13196/j.cims.2023.BPM25

计算机集成制造系统
中国兵器工业集团第210研究所

计算机集成制造系统

CSTPCD北大核心
影响因子：1.092
ISSN：1006-5911
年,卷(期)：2024.30(8)