Cloud storage systems are crucial for ensuring business stability and data reliability. Among them, block-based cloud storage systems (BCSSs) have been widely adopted in the industry due to their high efficiency and strong performance. However, system failures occur from time to time, causing significant financial losses to companies. Therefore, verifying the reliability of BCSSs has become important and urgent. Nevertheless, since blocks in these systems are of finite but variable sizes, it is difficult to describe and verify properties using first-order logic or separation logic. To address this issue, we propose Sequence-Heap Separation Logic (SeqSL), which introduces sequence values and sequence variables into separation logic. Our logic can simplify property expressions while enhancing the ability to describe these systems. To provide a theoretical foundation for verification, we study the decidability of this logic, with the main conclusions as follows. 1) The satisfiability problem of the fragment with a single quantifier alternation is decidable, and belongs to 2-EXPTIME (2-Exponential Time). As a by-product, we propose a decision procedure for this decidable fragment. 2) The satisfiability problem of the fragment with two quantifier alternations is undecidable.
Publications
- Article type
- Year
- Co-author
Article type
Year
Regular Paper
Issue
Journal of Computer Science and Technology 2025, 40(6): 1678-1692
Published: 01 November 2025
Total 1
京公网安备11010802044758号