{"id":14764,"date":"2020-07-02T12:06:48","date_gmt":"2020-07-02T10:06:48","guid":{"rendered":"http:\/\/localhost:8888\/clearsy\/offres\/validation-formelle-systeme\/"},"modified":"2021-07-02T15:41:40","modified_gmt":"2021-07-02T13:41:40","slug":"formal-system-validation","status":"publish","type":"offres","link":"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/","title":{"rendered":"Formal system validation"},"content":{"rendered":"<div class=\"wpb-content-wrapper\"><p>[vc_row][vc_column]<div class=\"text-bloc\"><p>The formal system verification, obtained with the B-method, is an element of the demonstration of the safety of a critical system.<\/p>\n<p>CLEARSY uses the detailed description of the design and algorithms used in the system under analysis in its procedure. The B models developed from these elements contain<\/p>\n<ul>\n<li>the mathematical formulation of the desired properties,<\/li>\n<li>the mathematical formulation of all necessary assumptions and<\/li>\n<li>the elements for conducting the proof.<\/li>\n<\/ul>\n<p>Once these models are proven with Workshop B, we are guaranteed that the desired properties are mathematically derived from the selected assumptions. These assumptions therefore constitute all the conditions sufficient to logically guarantee the desired properties. These conditions concern the design, the material and the context.<\/p>\n<p><span class=\"couleur_bleu txt_MAJ\">This process requires a detailed understanding of the real &#8220;why&#8221; of security<\/span>, thus requiring strong exchanges with the relevant business experts.<\/p>\n<p>For example, CLEARSY conducted a system verification with proof of the New York 7 line CBTC, using the B method.<\/p>\n<p>The proven system properties were:<br \/>\n<span class=\"couleur_bleu\">&gt; No collision between trains<\/span><br \/>\n<span class=\"couleur_bleu\">&gt; Impossibility of derailment on an unlocked switch<\/span><br \/>\n<span class=\"couleur_bleu\">&gt; Impossibility of overspeed<\/span><\/p>\n<\/div>[\/vc_column][\/vc_row]<\/p>\n<\/div>","protected":false},"excerpt":{"rendered":"<p>The formal system validation, obtained with the B-method, is an element of the demonstration of the safety of a critical system.<\/p>\n","protected":false},"featured_media":0,"template":"","domaine":[499],"class_list":["post-14764","offres","type-offres","status-publish","hentry","domaine-railway"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.3 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Formal system validation - 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\/offers\/formal-system-validation\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Formal system validation - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"The formal system validation, obtained with the B-method, is an element of the demonstration of the safety of a critical system.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:modified_time\" content=\"2021-07-02T13:41:40+00:00\" \/>\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\\\/offers\\\/formal-system-validation\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/offers\\\/formal-system-validation\\\/\",\"name\":\"Formal system validation - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\"},\"datePublished\":\"2020-07-02T10:06:48+00:00\",\"dateModified\":\"2021-07-02T13:41:40+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/offers\\\/formal-system-validation\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.clearsy.com\\\/en\\\/offers\\\/formal-system-validation\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/offers\\\/formal-system-validation\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Offers\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/offers\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Formal system validation\"}]},{\"@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 system validation - 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\/offers\/formal-system-validation\/","og_locale":"en_US","og_type":"article","og_title":"Formal system validation - CLEARSY","og_description":"The formal system validation, obtained with the B-method, is an element of the demonstration of the safety of a critical system.","og_url":"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/","og_site_name":"CLEARSY","article_modified_time":"2021-07-02T13:41:40+00:00","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\/offers\/formal-system-validation\/","url":"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/","name":"Formal system validation - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"datePublished":"2020-07-02T10:06:48+00:00","dateModified":"2021-07-02T13:41:40+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-system-validation\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"Offers","item":"https:\/\/www.clearsy.com\/en\/offers\/"},{"@type":"ListItem","position":3,"name":"Formal system validation"}]},{"@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\/offres\/14764","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/offres"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/offres"}],"version-history":[{"count":3,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/offres\/14764\/revisions"}],"predecessor-version":[{"id":17134,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/offres\/14764\/revisions\/17134"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=14764"}],"wp:term":[{"taxonomy":"domaine","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/domaine?post=14764"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}