Uniform Sampling of Timed Regular Expressions

Abstract

Systeme, die in Echtzeit und in der physischen Welt agieren, sind oft sensibel gegenüber der Reihenfolge und dem Timing von Ereignissen. Timed Regular Expressions (TRE) machen es möglich, komplexe Anforderungen an diese zeitlichen Abfolgen formal, aber dennoch intuitiv zu beschreiben. Für komplexe Systeme ist es meist unmöglich, formal zu beweisen, dass sie in allen Situationen korrekt arbeiten. Stattdessen werden sie gründlichen Tests unterzogen.Testen verfolgt üblicherweise eines von zwei Zielen: (1) kritische Testfälle finden bei denen das System Fehler macht, und (2) das Vertrauen in das System stärken, indem der Raum der Testfälle möglichst gut abgedeckt wird. Falsification Testing konzentriert sich dabei auf das erste Ziel, indem mittels Optimierungsmethoden effektiv problematische Testfälle gefunden werden. Wenn keine solchen Testfälle gefunden werden, gibt dieses Verfahren jedoch keine Information zur generellen Korrektheit des Systems. Das zweite Ziel, die Abdeckung der Testfälle zu garantieren, hat weniger Aufmerksamkeit erhalten.In dieser Arbeit wird eine neue Methode für diesen Zweck vorgestellt, in der wir die von einer TRE beschriebenen Testfälle zufällig und gleichverteilt (uniform) auswählen. So kann die Korrektheit des Systems probabilistisch garantiert werden. Wir entwickeln eine präzise Formalisierung von Volumen von TRE, die die Größe einer solchen Timed Language quantifizieren. Dieses Volumen wird verwendet, um den ersten gleichverteilten Sampling-Algorithmus zu entwickeln und die Korrektheit formal zu beweisen. Außerdem stellen wir eine neue Methode vor, in der durch gezieltes Rejection Sampling erstmals nichtdeterministische Sprachen mit einer Gleichverteilung versehen werden können. Diese Methode kann verwendet werden, um bestehende Sampling-Algorithmen für andere Formalismen zu verbessern, wie etwa Timed Automata. Wir stellen außerdem unsere Open-Source Tool-Implementierung für das gleichverteilte Sampling von TRE vor und demonstrieren in einigen Fallbeispielen, dass unsere Algorithmen praktisch einsetzbar sind.

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.