  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.
