# Time4sys2imi: A tool to formalize real-time system models under uncertainty

## TL;DR

Time4sys2imi is a tool that translates graphical real-time system models into formal automata, enabling schedulability analysis and timing constraint inference under uncertainty.

## Contribution

It introduces a translation from Time4sys to parametric timed automata, facilitating formal analysis of real-time systems.

## Key findings

- Successful application to various examples
- Enables schedulability checking and timing constraint inference
- Bridges graphical models with formal verification tools

## Abstract

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.