Formalizing Time4sys using parametric timed automata
This work addresses the need for formal verification in real-time systems modeling, but it is incremental as it builds on existing formalisms without introducing a new paradigm.
The authors tackled the lack of formal reasoning capabilities in the Time4sys modeling formalism for critical real-time systems by translating it to parametric timed automata, enabling formal verification.
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.