Formalizing Time4sys using parametric timed automata

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)International audienceCritical 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