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

• 作者: Jing Li Ming Zhu
• 来源期刊: 电脑和通信(英文)
• 学科: 工学
• 关键词: CONCURRENT System Verification CSP Process-Oriented PROGRAMMING ABSTRACTION CATEGORY Theory
• 年，卷（期）: dnhtxyw_2018,（11）
• 页码范围: 227-246
• 页数: 20页
• 分类号: TP39

摘要

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.