{"id":16171,"date":"2021-05-25T16:34:20","date_gmt":"2021-05-25T14:34:20","guid":{"rendered":"https:\/\/clearsy.matiere-1ere.fr\/?p=16171"},"modified":"2023-08-24T13:56:24","modified_gmt":"2023-08-24T11:56:24","slug":"the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods","status":"publish","type":"post","link":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/","title":{"rendered":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS"},"content":{"rendered":"<div class=\"wpb-content-wrapper\"><p>[vc_row][vc_column]<div class=\"text-bloc\"><p><strong>In order to analyse the safety of control system for the automatic lines 3 and 5 of Paris subway, CLEARSY has proceeded through event B method. The same method was employed previously for New-York subway.<\/strong><\/p>\n<p>Octys is a solution for automatic control of the railway traffic deployed by RATP on lines 3 and 5 of Paris subway. Like any CBTC (Communication Based Train System), Octys must guarantee a maximum-safety level (SIL4). Among others, it might be able to avoid any collision or derailment risks whatever may occur on subway lines (failures, signalisation, power supply, etc..). The subject-matter of the contract signed between CLEARSY and RATP was to prove formally the safety aspect of Octys through mathematical demonstration.<\/p>\n<p>For RATP, the fabrication of different Octys components should be achievable by different manufacturers, especially when it goes about such components as on-board and trackside. The consequence is that the global system safety doesn\u2019t result from finished products. \u00a0Because the guarantee of the assembly safety of different CBTC components, notably on-board and trackside, is a cross-systems specification examined by CLEARSY. Formal methods engineer at CLEARSY Julien Molinero explains: \u201c<em>We had to guarantee by proof, that when the specifications are met in a proper way by the subsystems then on-board\/trackside assembly is safe\u201d<\/em>. First, the system is described as a group of all elements that could evolve according to all specified events. Then it is necessary to communicate in mathematical language (formal B language) the required properties (non-collision, non-derailment) and to prove mathematically that the properties are conserved at any time. Otherwise, it is necessary to review the work by introducing more in detail the properties that the systems must respect.<\/p>\n<p>If the approach method remains innovative it means that its efficiency has been proved. CLEARSY has already demonstrated in the past that its ability to prove formally a complex system safety. Julien Molinero mentions: \u00ab<span>\u00a0<\/span><em>We have already carried out a similar project on New-York subway and managed to prove beyond doubt the CBTC safety implemented by the New York City Transit responsible for public transportation in New York.\u201d<\/em><span>\u00a0<\/span>\u00a0To date, CLEARSY mission for RATP allowed to complete some specification aspects and to provide clear and precise argumentation approving the safety of Octys solution.<\/p>\n<\/div>[\/vc_column][\/vc_row]<\/p>\n<\/div>","protected":false},"excerpt":{"rendered":"<p>In order to analyse the safety of control system for the automatic lines 3 and 5 of Paris subway, CLEARSY has proceeded through event B method.<\/p>\n","protected":false},"author":17,"featured_media":17202,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[682],"tags":[],"class_list":["post-16171","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-railway"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.3 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - 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\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"In order to analyse the safety of control system for the automatic lines 3 and 5 of Paris subway, CLEARSY has proceeded through event B method.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:published_time\" content=\"2021-05-25T14:34:20+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2023-08-24T11:56:24+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg\" \/>\n\t<meta property=\"og:image:width\" content=\"850\" \/>\n\t<meta property=\"og:image:height\" content=\"325\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"author\" content=\"Thierry Lecomte\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Thierry Lecomte\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/\"},\"author\":{\"name\":\"Thierry Lecomte\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/person\\\/62096c067e9d3a553ad93a906e95a673\"},\"headline\":\"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS\",\"datePublished\":\"2021-05-25T14:34:20+00:00\",\"dateModified\":\"2023-08-24T11:56:24+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/\"},\"wordCount\":393,\"commentCount\":0,\"publisher\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2021\\\/05\\\/B-OCTYS-web-US.jpeg\",\"articleSection\":[\"Railway\"],\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"CommentAction\",\"name\":\"Comment\",\"target\":[\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#respond\"]}]},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/\",\"name\":\"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2021\\\/05\\\/B-OCTYS-web-US.jpeg\",\"datePublished\":\"2021-05-25T14:34:20+00:00\",\"dateModified\":\"2023-08-24T11:56:24+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#primaryimage\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2021\\\/05\\\/B-OCTYS-web-US.jpeg\",\"contentUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2021\\\/05\\\/B-OCTYS-web-US.jpeg\",\"width\":850,\"height\":325},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/railway\\\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS\"}]},{\"@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\\\/\"}},{\"@type\":\"Person\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/person\\\/62096c067e9d3a553ad93a906e95a673\",\"name\":\"Thierry Lecomte\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g\",\"caption\":\"Thierry Lecomte\"},\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/author\\\/tlecomte\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - 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\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/","og_locale":"en_US","og_type":"article","og_title":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - CLEARSY","og_description":"In order to analyse the safety of control system for the automatic lines 3 and 5 of Paris subway, CLEARSY has proceeded through event B method.","og_url":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/","og_site_name":"CLEARSY","article_published_time":"2021-05-25T14:34:20+00:00","article_modified_time":"2023-08-24T11:56:24+00:00","og_image":[{"width":850,"height":325,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg","type":"image\/jpeg"}],"author":"Thierry Lecomte","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Thierry Lecomte","Est. reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#article","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/"},"author":{"name":"Thierry Lecomte","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/person\/62096c067e9d3a553ad93a906e95a673"},"headline":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS","datePublished":"2021-05-25T14:34:20+00:00","dateModified":"2023-08-24T11:56:24+00:00","mainEntityOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/"},"wordCount":393,"commentCount":0,"publisher":{"@id":"https:\/\/www.clearsy.com\/en\/#organization"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg","articleSection":["Railway"],"inLanguage":"en-US","potentialAction":[{"@type":"CommentAction","name":"Comment","target":["https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#respond"]}]},{"@type":"WebPage","@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/","url":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/","name":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg","datePublished":"2021-05-25T14:34:20+00:00","dateModified":"2023-08-24T11:56:24+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/05\/B-OCTYS-web-US.jpeg","width":850,"height":325},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/railway\/the-cbtc-octys-safety-analysed-by-clearsy-through-formal-methods\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"CLEARSY PROVED THE CBTC OCTYS SAFETY THROUGH FORMAL METHODS"}]},{"@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\/"}},{"@type":"Person","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/person\/62096c067e9d3a553ad93a906e95a673","name":"Thierry Lecomte","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/secure.gravatar.com\/avatar\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/1484587b45f9f96afa32a6615796f7bb4738001f5a3e0ebfe061e9a266f268a6?s=96&d=mm&r=g","caption":"Thierry Lecomte"},"url":"https:\/\/www.clearsy.com\/en\/author\/tlecomte\/"}]}},"_links":{"self":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/16171","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/users\/17"}],"replies":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/comments?post=16171"}],"version-history":[{"count":2,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/16171\/revisions"}],"predecessor-version":[{"id":19369,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/16171\/revisions\/19369"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/17202"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=16171"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/categories?post=16171"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/tags?post=16171"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}