STAGE Analyses de systèmes temps-réel à l'aide de Time4sys et IMITATOR

Date de mise à jour de l’offre

LIPN, Université Paris 13, Sorbonne Paris Cité :

Laboratoire d'informatique de Paris Nord

Description de la mission

OBJECTIF DU STAGE : Mettre au point une traduction automatique du formalisme Time4sys vers le langage d'entrée d'IMITATOR.



L'objectif du stage est de proposer une traduction automatique de Time4sys (langage mis au point par Thales) vers le langage d'entrée d'IMITATOR (logiciel de vérification de systèmes temps-réel) et ainsi de pouvoir analyser directement des modèles industriels grâce à IMITATOR.

IMITATOR est un logiciel développé au LIPN basé sur les automates temporisés paramétrés, un formalisme très puissant mais qui ne permet pas nativement de modéliser des systèmes temps-réel : des traductions sont nécessaires.

IMITATOR a ainsi permis de modéliser et vérifier plusieurs systèmes temps-réel en présence d'incertitude, avec des traductions ad-hoc venant de plusieurs formalismes



Des modifications d'IMITATOR lui-même (programmé en OCaml) sont envisageables si cela permet d'accélérer l'analyse du modèle obtenu.



version complète du sujet :

https://lipn.univ-paris13.fr/~andre/temp/stage-Astrei-fr.pdf

Profil recherché

Étudiant(e) de Master 2 recherche, Master 2 industrie ou écoles d'ingénieurs, en informatique ou réseaux ou systèmes temps-réel.

Niveau de qualification requis

Bac + 4/5 et +
  • Employeur
    LIPN, Université Paris 13, Sorbonne Paris Cité
  • Secteur d’activité de la structure
    Enseignement - Formation - Recherche
  • Effectif de la structure
    De 51 à 250 salariés
  • Site internet de la structure
    http://lipn.univ-paris13.fr/
  • Type de stage ou contrat
    Stage pour lycéens et étudiants en formation initiale
  • Date prévisionnelle de démarrage
  • Durée du stage ou contrat
    Plus de 4 mois et jusqu'à 6 mois
  • Le stage est-il rémunéré ?
    Oui
  • Niveau de qualification requis

    Bac + 4/5 et +
  • Lieu du stage
    Université Paris 13
    Av JB Clément
    93430 Villetaneuse
  • Accès et transports
    Station Villetaneuse-Université (T8 ou T11 express)