Uniform Sampling of Timed Regular Expressions

Systems that operate in the physical world and in real time are often sensitive to the order and timing of events. Timed Regular Expressions (TRE) are a powerful and intuitive formalism for specifying the intended temporal and timed behaviour of such real-time systems. Exhaustively verifying real-time systems in all possible situations is typically infeasible, hence testing is often the preferred analysis method in practice.
Testing typically has two complementary goals: (1) to efficiently find test cases in which the system fails, and (2) to gain confidence in the system’s correctness in the absence of failing tests by sufficiently covering the input space. Falsification testing is a popular approach that addresses the first objective by leveraging optimization techniques to efficiently detect faults in the system. Nevertheless, it typically does not provide much useful information if no failing test case is found. While much effort has been invested in the past in the falsification testing research, coverage-based testing has not received sufficient attention.
In this thesis, we focus on coverage testing and develop a method for uniformly sampling the input space of real-time systems provided in the form of TRE specifications. This method provides probabilistic guarantees for the system’s correctness. We first introduce a rigorous mathematical framework for computing volumes of TRE, real-valued measures that quantify the size of timed languages. Building on the idea of timed language volumes,
we develop the first direct uniform sampling algorithm for TRE specifications. Additionally, we propose a novel rejection-based technique for handling both nondeterministic specifications and the intersection operation, thus also enhancing existing uniform sampling methods for other real-time formalisms, such as Timed Automata. We implement the methods developed in this thesis in VolTRE, an open-source tool for sampling from TRE, demonstrating the practical use of our research outcomes in several case studies.