Formalizing Time4sys using parametric timed automata
Software Engineering
2019-07-31 v1 Formal Languages and Automata Theory
Abstract
Critical real-time systems must be verified to avoid the risk of dramatic consequences in case of failure. Thales developed an open formalism Time4sys to model real-time systems, with expressive features such as periodic or sporadic tasks, task dependencies, distributed systems, etc. However, Time4sys does not natively allow for a formal reasoning. In this work, we present a translation from Time4sys to (parametric) timed automata, so as to allow for a formal verification.
Keywords
Cite
@article{arxiv.1905.09458,
title = {Formalizing Time4sys using parametric timed automata},
author = {Étienne André},
journal= {arXiv preprint arXiv:1905.09458},
year = {2019}
}
Comments
This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE 2019)