An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems

TL;DR

This paper introduces an event-based rely-guarantee formalization in Isabelle/HOL for verifying concurrent reactive systems, effectively handling multicore and interruptible concurrency with case studies.

Contribution

It presents a novel formal approach and proof system for concurrent reactive systems using event-based rely-guarantee reasoning in Isabelle/HOL, addressing limitations of prior imperative-focused methods.

Findings

Successfully formalized the approach in Isabelle/HOL.

Proved the soundness of the proof system.

Validated with case studies on multicore and interruptible systems.

Abstract

Reactive systems are composed of a well defined set of input events that the system reacts with by executing an associated handler to each event. In concurrent environments, event handlers can interact with the execution of other programs such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. State of the art rely-guarantee based verification frameworks only focus on imperative programs, being difficult to capture in the rely and guarantee relations interactions with possible infinite sequences of event handlers, and the input arguments to event handlers. In this paper, we propose the formalisation in Isabelle/HOL of an event-based rely-guarantee approach for concurrent reactive systems. We develop a Pi-Core language which incorporates a concurrent imperative and system specification language by `events', and we build a rely-guarantee proof system for Pi-Core and prove its soundness. Our approach can deal with multicore and interruptible concurrency. We use two case studies to show this: an interruptible controller for stepper motors and an ARINC 653 multicore kernel, and prove the functional correctness and preservation of invariants of them in Isabelle/HOL.