# Formalizing Time4sys using parametric timed automata

## TL;DR

This paper introduces a translation from the Time4sys formalism to parametric timed automata, enabling formal verification of complex real-time systems modeled in Time4sys.

## Contribution

It provides the first systematic method to formalize Time4sys models using parametric timed automata for verification purposes.

## Key findings

- Enables formal verification of Time4sys models.
- Supports complex real-time system features.
- Facilitates automated analysis and validation.

## 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.