{"id":468,"date":"2023-09-28T15:09:33","date_gmt":"2023-09-28T15:09:33","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=468"},"modified":"2023-10-02T07:54:11","modified_gmt":"2023-10-02T07:54:11","slug":"des-langages-de-programmation-formels-pour-le-logiciel-temps-reel","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/?page_id=468","title":{"rendered":"Des langages de programmation formels pour le logiciel temps r\u00e9el"},"content":{"rendered":"\n<h2 class=\"wp-block-heading\"><img loading=\"lazy\" decoding=\"async\" class=\"alignright\" src=\"https:\/\/www.di.ens.fr\/~pouzet\/mp.jpg\" width=\"150\" height=\"300\"><a href=\"https:\/\/www.di.ens.fr\/~pouzet\/\">Marc Pouzet<\/a>, <a href=\"https:\/\/www.di.ens.fr\/\">DIENS<\/a>, <a href=\"https:\/\/www.ens.psl.eu\/\">ENS Paris<\/a> et <a href=\"https:\/\/www.inria.fr\/\">INRIA<\/a> \u00e9quipe <a href=\"https:\/\/parkas.di.ens.fr\/\">PARKAS<\/a><\/h2>\n\n\n\n<div class=\"wp-block-group is-vertical is-layout-flex wp-container-core-group-is-layout-8cf370e7 wp-block-group-is-layout-flex\">\n<div data-wp-interactive=\"core\/file\" class=\"wp-block-file\"><object data-wp-bind--hidden=\"!state.hasPdfPreview\" hidden class=\"wp-block-file__embed\" data=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/wp-content\/uploads\/2023\/10\/expose.marc_compressed.pdf\" type=\"application\/pdf\" style=\"width:100%;height:360px\" aria-label=\"Embed of Les transparents sont ici:.\"><\/object><a id=\"wp-block-file--media-8d72ccb6-21bc-4ae6-9d2d-b59c96caf02f\" href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/wp-content\/uploads\/2023\/10\/expose.marc_compressed.pdf\">Les transparents sont ici:<\/a><a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/wp-content\/uploads\/2023\/10\/expose.marc_compressed.pdf\" class=\"wp-block-file__button wp-element-button\" download aria-describedby=\"wp-block-file--media-8d72ccb6-21bc-4ae6-9d2d-b59c96caf02f\">Download<\/a><\/div>\n<\/div>\n\n\n\n<p>Le fichier <code><a href=\"https:\/\/cloud.lsv.ens-paris-saclay.fr\/public.php?service=files&amp;t=fb1a95aa105b5e8aed069cd99d4d2e8c\">kahn.hs<\/a><\/code> et le fichier <code><a href=\"https:\/\/cloud.lsv.ens-paris-saclay.fr\/public.php?service=files&amp;t=0a03346de984e99fbfddbd45a9f7c98e\">kahn_lazy.ml<\/a><\/code> de la d\u00e9mo (transparent 27\/45).<\/p>\n\n\n\n<p><strong>R\u00e9sum\u00e9.<\/strong>  On trouve aujourd&#8217;hui du logiciel temps r\u00e9el dans les avions, les trains et les voitures. E.g., commandes de vol, syst\u00e8me de freinage et contr\u00f4le moteur d&#8217;avion; contr\u00f4le de bord et gestion de la position d&#8217;un train; gestion de l&#8217;\u00e9nergie d&#8217;une voiture \u00e9lectrique, pour n&#8217;en citer que quelques uns. Ce logiciel est complexe \u2014 quelques millions de lignes de code pour les commandes de vol d&#8217;un avion moderne \u2014 et il est difficile \u00e0 concevoir ou \u00e0 tester car il interagit avec un environnement physique qui n&#8217;est connu que partiellement. Enfin, il doit r\u00e9pondre \u00e0 des exigences de s\u00fbret\u00e9 rigoureuses et v\u00e9rifiables par des autorit\u00e9s ind\u00e9pendantes, comme l&#8217;imposent l&#8217;avionique civile et le ferroviaire, par exemple.<\/p>\n\n\n\n<p>La science informatique s&#8217;est int\u00e9ress\u00e9e d\u00e8s la fin des ann\u00e9es 70 \u00e0 cette question essentielle: comment programmer le logiciel temps r\u00e9el et dans quel langage afin que le programme soit pr\u00e9cis, qu&#8217;il autorise des raisonnements formels ind\u00e9pendants de toute impl\u00e9mentation et que le code produit par le compilateur soit correct, qu&#8217;il s&#8217;ex\u00e9cute de mani\u00e8re d\u00e9terministe, sans blocage et respecte les contraintes de temps r\u00e9el?<\/p>\n\n\n\n<p>Dans cet expos\u00e9, nous montrerons la gen\u00e8se du mod\u00e8le de programmation synchrone jusqu&#8217;\u00e0 son utilisation aujourd&#8217;hui pour d\u00e9velopper de nombreux logiciels d&#8217;applications temps r\u00e9el critiques.<\/p>\n\n\n\n<p>Nous rappellerons sa filiation avec les mod\u00e8les et outils anciens de l&#8217;automatique ainsi que ceux de la th\u00e9orie des langages, les principes du mod\u00e8le et son int\u00e9gration dans plusieurs langages d\u00e9di\u00e9s.<\/p>\n\n\n\n<p>Nous montrerons quelques unes des questions de recherche qui se sont pos\u00e9es et les \u00e9volutions majeures que les langages synchrones ont connu.<\/p>\n\n\n\n<p>Nous montrerons deux pistes de recherche plus r\u00e9centes. L&#8217;une est le d\u00e9veloppement d&#8217;un compilateur d&#8217;un langage synchrone r\u00e9aliste avec une preuve formellement v\u00e9rifi\u00e9e que le code produit est correct vis-\u00e0-vis du code source. L&#8217;autre vise \u00e0 \u00e9tendre l&#8217;expressivit\u00e9 du langage pour d\u00e9crire des syst\u00e8mes hybrides combinant du temps discret et du temps continu, en particulier l&#8217;interaction entre le logiciel et son environnement physique. On vise ici l&#8217;\u00e9criture de mod\u00e8les que l&#8217;on pourra tester et valider avec une plus grande fid\u00e9lit\u00e9 vis-\u00e0-vis du syst\u00e8me r\u00e9el final.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Marc Pouzet, DIENS, ENS Paris et INRIA \u00e9quipe PARKAS Le fichier kahn.hs et le fichier kahn_lazy.ml de la d\u00e9mo (transparent 27\/45). R\u00e9sum\u00e9. On trouve aujourd&#8217;hui du logiciel temps r\u00e9el dans les avions, les trains et les voitures. E.g., commandes de vol, syst\u00e8me de freinage et contr\u00f4le moteur d&#8217;avion; contr\u00f4le de bord et gestion de la [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-468","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/468","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=468"}],"version-history":[{"count":7,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/468\/revisions"}],"predecessor-version":[{"id":480,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=\/wp\/v2\/pages\/468\/revisions\/480"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/confsrentree\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=468"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}