论文标题
扩展并发的分离逻辑以增强模块化形式化
Extending Concurrent Separation Logic to Enhance Modular Formalization
论文作者
论文摘要
如今，已经开发了许多基于大规模分布式系统的服务，以提高人类生活的便利性。另一方面，由于复杂和嵌套的体系结构，确保这些系统的正确性和特性成为一个重大挑战。尽管并发分离逻辑（CSL）通过指定系统并验证它们的正确性来部分解决问题，但它面临模块化问题。在本文中，我们提出了一个扩展的并发分离逻辑（ECSL），以在时间扩展，通信扩展，环境扩展和嵌套扩展的支持下解决CSL的模块化问题。 ECSL能够以极大的模块化从内存管理到体系结构和协议设计的不同抽象级别的系统形式化系统。此外，我们在开发ECSL时坚持单位性和兼容性原则。
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.
