Towards a Categorical Framework for Verifying Design and Implementation of Concurrent Systems  

作　　者：Ming Zhu Jing Li 

机构地区：[1]College of Computer Science and Technology, Shandong University of Technology, Zibo, China

出　　处：《Journal of Computer and Communications》2018年第11期227-246,共20页电脑和通信（英文）

摘　　要：Process-oriented design and implementation of concurrent systems has important benefits. However, the inherent complexity of concurrent processes’ communication imposes challenges such as verifying consistency between the process-oriented design and implementation of a concurrent system. To deal with such a challenge, we use Galois connections, Failures and Category Theory to construct a formal framework for designing, implementing, analyzing and verifying consistency of concurrent systems. For the purpose of illustrating the framework, a running concurrent system is designed by Communicating Sequential Processes, implemented by a process-oriented programming language Erasmus.Process-oriented design and implementation of concurrent systems has important benefits. However, the inherent complexity of concurrent processes’ communication imposes challenges such as verifying consistency between the process-oriented design and implementation of a concurrent system. To deal with such a challenge, we use Galois connections, Failures and Category Theory to construct a formal framework for designing, implementing, analyzing and verifying consistency of concurrent systems. For the purpose of illustrating the framework, a running concurrent system is designed by Communicating Sequential Processes, implemented by a process-oriented programming language Erasmus.

关 键 词：CONCURRENT System Verification CSP Process-Oriented PROGRAMMING ABSTRACTION CATEGORY Theory 

分 类 号：TP39[自动化与计算机技术—计算机应用技术]