Time distance based computation of the state space of preemptive real time systems

TL;DR

This paper introduces a novel time distance-based method for overapproximating the state space of preemptive real-time systems, resulting in tighter, more efficient graphs that preserve quantitative timing properties.

Contribution

It extends the state space overapproximation technique by incorporating time distance systems, improving accuracy and computational efficiency.

Findings

Graphs are of similar size to exact graphs.

Computation times are significantly reduced.

Tighter approximation improves model analysis.

Abstract

We explore in this paper a novel approach that builds an overapproximation of the state space of preemptive real time systems. Our graph construction extends the expression of a class to the time distance system that encodes the quantitative properties of past fired subsequences. This makes it possible to restore relevant time information that is used to tighten still more the DBM overapproximation of reachable classes. We succeed thereby to build efficiently tighter approximated graphs which are more appropriate to restore the quantitative properties of the model. The simulation results show that the computed graphs are of the same size as the exact graphs while improving by far the times needed for their computation.