Partagez sur
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
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 +
Les offres de stage ou de contrat sont définies par les recruteurs eux-mêmes.
En sa qualité d’hébergeur dans le cadre du dispositif des « 100 000 stages », la Région Île-de-France est soumise à un régime de responsabilité atténuée prévu aux articles 6.I.2 et suivants de la loi n°2204-575 du 21 juin 2004 sur la confiance dans l’économie numérique.
La Région Île-de-France ne saurait être tenue responsable du contenu des offres.
Néanmoins, si vous détectez une offre frauduleuse, abusive ou discriminatoire vous pouvez la signaler
en cliquant sur ce lien.
-
EmployeurLIPN, Université Paris 13, Sorbonne Paris Cité
-
Secteur d’activité de la structureEnseignement - Formation - Recherche
-
Effectif de la structureDe 51 à 250 salariés
-
Site internet de la structurehttp://lipn.univ-paris13.fr/
-
Type de stage ou contratStage pour lycéens et étudiants en formation initiale
-
Date prévisionnelle de démarrage
-
Durée du stage ou contratPlus 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 stageUniversité Paris 13 Av JB Clément
93430 Villetaneuse -
Accès et transportsStation Villetaneuse-Université (T8 ou T11 express)