An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems
This work addresses verification difficulties for concurrent reactive systems, such as those in embedded or multicore environments, by extending rely-guarantee methods to handle event-based interactions, though it is incremental as it builds on existing verification frameworks.
The paper tackles the challenge of verifying concurrent reactive systems, which involve complex interactions between event handlers, by proposing an event-based rely-guarantee approach formalized in Isabelle/HOL, and demonstrates its applicability through case studies on a stepper motor controller and an ARINC 653 multicore kernel, proving functional correctness and invariant preservation.
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.