Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation

Andrea Manini, Matteo Rossi, Pierluigi San Pietro

TL;DR

The paper tackles the oracle problem in testing model checkers for Timed Automata by introducing a modular framework based on Tiled Timed Automata ($\mathrm{TTA}$) and automated oracle generation via Weighted Automata. It implements TABEC to validate emptiness checking for a decidable PTA variant ($\mathrm{PnrtTA}$) using randomly generated $\mathrm{PTTA}$ tests and predicted parameter intervals. It provides a decidability result for $\mathrm{PnrtTA}$ emptiness, reduces the problem to a finite set of TA emptiness checks, and extends the approach to min-cost reachability for Priced Timed Automata, supported by empirical scalability analyses. Overall, the framework offers a general, adaptable method for verifying TA model checkers across variants and problems, enabling systematic, oracle-backed testing and future extensions.

Abstract

A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is expected. Indeed, these tools are frequently novel and may not have been thoroughly tested. When standard benchmarks may be insufficient or unavailable, random test case generation offers a promising approach. To scale up, random testing requires comparing actual versus expected results, i.e., solving the oracle problem. To address this challenge, this work introduces a novel theoretical framework based on a modular variant of Timed Automata (TA), called Tiled Timed Automata (TTA), for testing model checkers operating with variations of TA, by building oracles based on Weighted Automata. The framework is initially applied to verify model checkers solving the emptiness problem for Parametric TA and it is validated, in this specific scenario, by our tool, TABEC, which randomly generates tests predicting their expected outcome through automated oracle generation. Furthermore, the general nature of TTA facilitates the framework adaptation to model checkers solving other decidable problems on TA, as detailed for the minimum-cost reachability problem of Priced TA.

Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation

TL;DR

The paper tackles the oracle problem in testing model checkers for Timed Automata by introducing a modular framework based on Tiled Timed Automata () and automated oracle generation via Weighted Automata. It implements TABEC to validate emptiness checking for a decidable PTA variant () using randomly generated tests and predicted parameter intervals. It provides a decidability result for emptiness, reduces the problem to a finite set of TA emptiness checks, and extends the approach to min-cost reachability for Priced Timed Automata, supported by empirical scalability analyses. Overall, the framework offers a general, adaptable method for verifying TA model checkers across variants and problems, enabling systematic, oracle-backed testing and future extensions.

Abstract

A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is expected. Indeed, these tools are frequently novel and may not have been thoroughly tested. When standard benchmarks may be insufficient or unavailable, random test case generation offers a promising approach. To scale up, random testing requires comparing actual versus expected results, i.e., solving the oracle problem. To address this challenge, this work introduces a novel theoretical framework based on a modular variant of Timed Automata (TA), called Tiled Timed Automata (TTA), for testing model checkers operating with variations of TA, by building oracles based on Weighted Automata. The framework is initially applied to verify model checkers solving the emptiness problem for Parametric TA and it is validated, in this specific scenario, by our tool, TABEC, which randomly generates tests predicting their expected outcome through automated oracle generation. Furthermore, the general nature of TTA facilitates the framework adaptation to model checkers solving other decidable problems on TA, as detailed for the minimum-cost reachability problem of Priced TA.

Paper Structure

This paper contains 5 sections, 1 theorem, 1 figure.

Table of Contents

  1. Introduction
  2. Theoretical background
  3. (Parametric) Timed Automata
  4. Decidability of PnrtTA
  5. Weighted Automata

Key Result

theorem thmcountertheorem

Let $\mathcal{A}$ be a PnrtTA and $C$ be the largest constant appearing in the guards of $\mathcal{A}$. Then:

Figures (1)

  • Figure 1: Example of PnrtTA, where $\Sigma = \{a\}$, $X = \{x, y\}$, and $P = \{\mu\}$. Clock resets are represented in bold, while clock guards are represented in italic. The initial location is $q_0$, while the (only) accepting location is $q_2$.

Theorems & Definitions (3)

  • definition thmcounterdefinition: Timed Automaton
  • definition thmcounterdefinition: Non-resetting test TA
  • theorem thmcountertheorem