Over-approximation of weakly-hard constraints for control systems verification (Extended)

TL;DR

This paper introduces an over-approximation method for weakly-hard constraints in control systems, enabling sound safety verification where minimal automata are too large to handle.

Contribution

It proposes a compressed language acceptor that over-approximates weakly-hard constraints, facilitating verification of complex control systems.

Findings

The new acceptor can be embedded in control design workflows.

Empirical results show improved verification capabilities.

The approach provides sound safety guarantees for systems beyond current methods.

Abstract

A hard real-time system cannot miss any deadline. A weakly-hard real-time system, on the contrary, is designed to tolerate a specific number of deadline misses. For instance, the AnyMiss(2, 300) weakly-hard constraint stipulates that in every window of 300 consecutive jobs, at most 2 deadlines are missed. The weakly-hard model is the state-of-the-art for industrial dependability-by-design of control systems that tolerate deterministic failures. Weakly-hard constraints correspond to regular languages. The size of the minimal finite state machine that recognizes whether a string satisfies the constraint (about 45k states for AnyMiss(2, 300)) is a notorious impediment for the verification of control system properties. This paper discusses an over-approximation of the language that allows us to provide sound safety guarantees for control systems under deadline misses that would be out of reach using the minimal finite state machine. We present a compressed language acceptor and prove that it simulates the original finite state machine. We study language cardinality properties, and report on empirical results that show how the new acceptor can be embedded in the control design workflow, leading to verifying safety for systems for which the state-of-the-art tools do not provide answers.