Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications

TL;DR

PiCore is a rely-guarantee reasoning framework that enables formal specification and verification of complex concurrent reactive systems, supporting heterogeneous languages and real-world applications like RTOS memory management and business process translation.

Contribution

The paper introduces PiCore, a flexible rely-guarantee framework that integrates multiple languages and proof systems for verifying complex CRSs at different abstraction levels.

Findings

Successfully integrated two existing languages with PiCore without modifications.

Applied PiCore to verify concurrent memory management in Zephyr RTOS.

Verified translation of BPEL to PiCore for business process systems.

Abstract

The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, specifications using heterogeneous reaction patterns, different abstraction levels, and the complexity of real-world CRSs are still challenging the rely-guarantee approach. This article proposes PiCore, a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach the specification and logic of reactive aspects of CRSs from event behaviours. PiCore parametrizes the language and its rely-guarantee system for event behaviour using a rely-guarantee interface and allows to easily integrate 3rd-party languages via rely-guarantee adapters. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs. PiCore has been applied to two real-world case studies, i.e. formal verification of concurrent memory management in Zephyr RTOS and a verified translation for a standardized Business Process Execution Language (BPEL) to PiCore.