Exemplifying parametric timed specifications over signals with bounded behavior

TL;DR

This paper introduces an automated method to generate concrete examples of behaviors that satisfy or violate complex timed specifications expressed as automata with timing constraints and parameters, aiding in property verification.

Contribution

It presents a novel approach to exemplify properties specified by extended automata with timing and signal constraints, facilitating analysis of real-valued signals and hybrid automata.

Findings

Successfully generates concrete runs exemplifying specifications

Handles automata with timing parameters and signal constraints

Applicable to rectangular hybrid automata

Abstract

Specifying properties can be challenging work. In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraints and timing parameters, and that can also encode constraints over real-valued signals. That is, given such a specification and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this specification. Specifically, our method takes as input a specification, and a set of admissible behaviors, all given as a subclass of rectangular hybrid automata, namely timed automata extended with arbitrary clock rates, signal constraints, and timing parameters. Our method then generates concrete runs exemplifying the specification.