Extending Concurrent Separation Logic to Enhance Modular Formalization

TL;DR

This paper introduces ECSL, an extended form of concurrent separation logic, to improve modularity in formal verification of complex distributed systems across multiple abstraction levels.

Contribution

The paper proposes ECSL, an extension of CSL that incorporates temporal, communication, environment, and nest extensions to enhance modularity and formalization capabilities.

Findings

ECSL formalizes systems from memory to architecture and protocol design.

ECSL maintains unitarity and compatibility principles.

ECSL improves modularity in system verification.

Abstract

Nowadays, numerous services based on large-scale distributed systems have been developed to boost the convenience of human life. On the other side, it becomes a significant challenge to ensure the correctness and properties of these systems due to the complex and nested architecture. Although concurrent separation logic (CSL) has partially tackled the problem by specifying systems and verifying the correctness of them, it faces modularity issues. In this paper, we propose an extended concurrent separation logic (ECSL) to address the modularity issues of CSL with the support of the temporal extension, communication extension, environment extension, and nest extension. ECSL is capable of formalizing systems at different abstraction levels from memory management to architecture and protocol design with great modularity. Furthermore, we stick to unitarity and compatibility principles while developing ECSL.