Verification Method of Asynchronously Communicating Programs Based on Basic Parallel Processes
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Asynchronously communicating program is the program that processes achieve non-blocking concurrency through asynchronous message passing. At present, the verification problem of asynchronously communicating program is usually reduced to vector addition system and its extension model, so it has high complexity and lack of efficient tools. Basic Parallel Processes, as a subclass of vector addition system, whose verification of complexity reachability is NP-complete, can also be used as an important model for verifying concurrent programs. Firstly, improve the Actor communicating system proposed by Osualdo, et al., by reducing it to Basic Parallel Processes. Then, realizing an automatic model checker for basic parallel processes named RABLE. The experimental results show that the verification method is more efficient than the existing tools for a series of program verification problems of asynchronously communicating programs.

    Reference
    Related
    Cited by
Get Citation

赵樱,谭锦豪,李国强.基于基本并行进程的异步通信程序的验证方法.软件学报,2022,33(8):2782-2796

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 04,2021
  • Revised:October 14,2021
  • Adopted:
  • Online: January 28,2022
  • Published: August 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063