Exemplifying parametric timed specifications over signals with bounded behavior
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.
Keywords
Cite
@article{arxiv.2203.13247,
title = {Exemplifying parametric timed specifications over signals with bounded behavior},
author = {Étienne André and Masaki Waga and Natsuki Urabe and Ichiro Hasuo},
journal= {arXiv preprint arXiv:2203.13247},
year = {2022}
}
Comments
This is the author (and extended) version of the manuscript of the same name published in the proceedings of the 14th NASA Formal Methods Symposium (NFM 2022). This work is partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST and by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015)