Verification of Configurable SRA Systems

TL;DR

This paper presents a contract-based deductive verification method for configurable scheduler-restricted asynchronous systems, enabling the proof of correctness across all possible configurations using the Dafny verifier.

Contribution

It introduces a novel compositional verification approach combining abstraction, summarization, and simplification for configurable SRA systems, scalable to industrial case studies.

Findings

Effective verification of complex industrial systems

Scales to unbounded families of system configurations

Automates reasoning about parameterized behaviors

Abstract

Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.