{"id":14819,"date":"2020-07-24T17:11:14","date_gmt":"2020-07-24T15:11:14","guid":{"rendered":"http:\/\/localhost:8888\/clearsy\/references\/pmi-l1\/"},"modified":"2021-06-01T14:06:25","modified_gmt":"2021-06-01T12:06:25","slug":"pmi-l1","status":"publish","type":"references","link":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/","title":{"rendered":"Formal verification of RATP interlocking systems"},"content":{"rendered":"\r\n\r\n\r\n<ul class=\"wp-block-list\"><\/ul>\r\n\r\n\r\n\r\n<p class=\"lanceur\">The PMI L1 project consists of creating a process to check the computer signalling implemented on line 1, 3 bis and 11 of the Paris metro.<\/p>\r\n<ul>\r\n<li><strong>CLIENT :<\/strong> RATP, AQL<\/li>\r\n<li><strong>DATE :<\/strong> From November 2007 to today<\/li>\r\n<li><strong>LOCATION :<\/strong> Line 1, 3bis et 11, Paris Metro<\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<p>This process is based on a formal approach, and necessitated the development of a proof workshop adapted to the Thal\u00e8s RSS computerised signal boxes (PMI). This workshop has been constructed around the Prover iLock Verifier proof engine by Prover Technology and certified with CENELEC SIL4 software security.<\/p>\r\n\r\n\r\n\r\n<p>Trials have been carried out on the PMI data from lines 11 and 3 bis of the Parisian metro. This workshop is currently used within the framework of the PMI L1 project for checking certain security properties on the PMI, which will soon be installed on line 1 of the Paris metro.<\/p>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Our actions<\/h2>\r\n\r\n\r\n\r\n<p class=\"lanceur\">CLEARSY has contributed to the SIL4 evaluation of the tooling making up the Prover iLock proof workshop \u2013 PMI. CLEARSY has also participated in the modelling and the proof of certain safety properties on the PMI of lines 11, 3 bis and 1.<\/p>\r\n\r\n\r\n\r\n<p>Indeed, CLEARSY has participated in the verification of proof carried out by Thal\u00e8s RSS on the PMI of line 1. We are continuing to assist the RATP in verifying the proof of Thal\u00e8s RSS and for the proof of certain properties within the context of the PMI L1 project.-.<\/p>\r\n","protected":false},"excerpt":{"rendered":"<p>The PMI L1 project consists of creating a process to check the computer signalling implemented on line 1, 3 bis [&hellip;]<\/p>\n","protected":false},"featured_media":15048,"template":"","secteur":[],"domaines_references":[],"class_list":["post-14819","references","type-references","status-publish","has-post-thumbnail","hentry"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.3 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Formal verification of RATP interlocking systems - CLEARSY<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Formal verification of RATP interlocking systems - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"The PMI L1 project consists of creating a process to check the computer signalling implemented on line 1, 3 bis [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:modified_time\" content=\"2021-06-01T12:06:25+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/ratp.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"1170\" \/>\n\t<meta property=\"og:image:height\" content=\"615\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/\",\"name\":\"Formal verification of RATP interlocking systems - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/07\\\/ratp.jpg\",\"datePublished\":\"2020-07-24T15:11:14+00:00\",\"dateModified\":\"2021-06-01T12:06:25+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/#primaryimage\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/07\\\/ratp.jpg\",\"contentUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/07\\\/ratp.jpg\",\"width\":1170,\"height\":615,\"caption\":\"Syst\u00e8me automatique d\u2019exploitation des trains, ligne 1 (SAET L1)\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/pmi-l1\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"References\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/references\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Formal verification of RATP interlocking systems\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\",\"name\":\"CLEARSY\",\"description\":\"Safety Solutions Designer\",\"publisher\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"},{\"@type\":\"Organization\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\",\"name\":\"CLEARSY\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/logo\\\/image\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/04\\\/logo-clearsy.svg\",\"contentUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/04\\\/logo-clearsy.svg\",\"width\":652,\"height\":163,\"caption\":\"CLEARSY\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/logo\\\/image\\\/\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Formal verification of RATP interlocking systems - CLEARSY","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/","og_locale":"en_US","og_type":"article","og_title":"Formal verification of RATP interlocking systems - CLEARSY","og_description":"The PMI L1 project consists of creating a process to check the computer signalling implemented on line 1, 3 bis [&hellip;]","og_url":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/","og_site_name":"CLEARSY","article_modified_time":"2021-06-01T12:06:25+00:00","og_image":[{"width":1170,"height":615,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/ratp.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/","url":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/","name":"Formal verification of RATP interlocking systems - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/ratp.jpg","datePublished":"2020-07-24T15:11:14+00:00","dateModified":"2021-06-01T12:06:25+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/ratp.jpg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/ratp.jpg","width":1170,"height":615,"caption":"Syst\u00e8me automatique d\u2019exploitation des trains, ligne 1 (SAET L1)"},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/references\/pmi-l1\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"References","item":"https:\/\/www.clearsy.com\/en\/references\/"},{"@type":"ListItem","position":3,"name":"Formal verification of RATP interlocking systems"}]},{"@type":"WebSite","@id":"https:\/\/www.clearsy.com\/en\/#website","url":"https:\/\/www.clearsy.com\/en\/","name":"CLEARSY","description":"Safety Solutions Designer","publisher":{"@id":"https:\/\/www.clearsy.com\/en\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.clearsy.com\/en\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"},{"@type":"Organization","@id":"https:\/\/www.clearsy.com\/en\/#organization","name":"CLEARSY","url":"https:\/\/www.clearsy.com\/en\/","logo":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/logo\/image\/","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/04\/logo-clearsy.svg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/04\/logo-clearsy.svg","width":652,"height":163,"caption":"CLEARSY"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/logo\/image\/"}}]}},"_links":{"self":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/references\/14819","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/references"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/references"}],"version-history":[{"count":1,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/references\/14819\/revisions"}],"predecessor-version":[{"id":16259,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/references\/14819\/revisions\/16259"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/15048"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=14819"}],"wp:term":[{"taxonomy":"secteur","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/secteur?post=14819"},{"taxonomy":"domaines_references","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/domaines_references?post=14819"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}