Time4sys2imi: A tool to formalize real-time system models under uncertainty
This work addresses the need for formal verification in real-time system design, particularly for engineers using Time4sys, though it appears incremental as it builds on existing formalisms.
The authors tackled the problem of formal analysis for real-time systems by developing Time4sys2imi, a tool that translates Time4sys models into parametric timed automata for IMITATOR, enabling schedulability checks and inference of timing constraints.
Time4sys is a formalism developed by Thales, realizing a graphical specification for real-time systems. However, this formalism does not allow to perform formal analyses for real-time systems. So a translation of this tool to a formalism equipped with a formal semantics is needed. We present here Time4sys2imi, a tool translating Time4sys models into parametric timed automata in the input language of IMITATOR. This translation allows not only to check the schedulability of real-time systems, but also to infer some timing constraints (e.g., deadlines, offsets) guaranteeing schedulability. We successfully applied Time4sys2imi to various examples.