A Categorical Approach to Verifying Consistency in Concurrent Systems

A concurrent system involves several executing components. Such a system usually allows to carry out multiple tasks at the same time, which can speed up the computational work of software substantially. The recent research findings demonstrate that process-oriented programming languages provide a suitable means for developing concurrent systems. However, design and implementation are at different levels of abstraction in software development process. It is challenging to incorporate knowledge and experience to control the consistency between these phases in developing concurrent systems. The potential inconsistencies arising would introduce errors to the production of concurrent systems, which would prove fatal to the systems in areas with zero tolerance for failure. To tackle such a challenge, the goal of this research is to propose an innovative categorical framework for designing, implementing and verifying the consistency of communications. This framework is inspired by Hoare's vision of category theory and obtained research results towards validating the vision. In this framework, Communicating Sequential Processes(CSP) and Erasmus are used for design and implementation. In addition, abstract interpretation is employed to extract process communications from implementation. Furthermore, several novel rules to analyze semantics of abstraction of implementation are proposed for Erasmus. Finally, category theory is utilized as an innovative means to model and verify consistency of process communications. The framework is illustrated by using several running examples