English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The rely-guarantee approach is a promising way for compositional verificationof concurrent reactive systems (CRSs), e.g. concurrent operating systems,interrupt-driven control systems and business process systems. However,specifications using heterogeneous reaction patterns, different abstractionlevels, and the complexity of real-world CRSs are still challenging therely-guarantee approach. This article proposes PiCore, a rely-guaranteereasoning framework for formal specification and verification of CRSs. Wedesign an event specification language supporting complex reaction structuresand its rely-guarantee proof system to detach the specification and logic ofreactive aspects of CRSs from event behaviours. PiCore parametrizes thelanguage and its rely-guarantee system for event behaviour using arely-guarantee interface and allows to easily integrate 3rd-party languages viarely-guarantee adapters. By this design, we have successfully integrated twoexisting languages and their rely-guarantee proof systems without any change oftheir specification and proofs. PiCore has been applied to two real-world casestudies, i.e. formal verification of concurrent memory management in ZephyrRTOS and a verified translation for a standardized Business Process ExecutionLanguage (BPEL) to PiCore.

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