{"id":14796,"date":"2020-07-24T14:54:02","date_gmt":"2020-07-24T12:54:02","guid":{"rendered":"http:\/\/localhost:8888\/clearsy\/offres\/formal-analysis-of-software\/"},"modified":"2022-04-14T18:12:52","modified_gmt":"2022-04-14T16:12:52","slug":"formal-analysis-of-software","status":"publish","type":"offres","link":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/","title":{"rendered":"Formal analysis and validation of software"},"content":{"rendered":"\r\n<p class=\"lanceur\">CLEARSY proposes a new innovative analysis approach to establish with mathematical proof that all or part of a software are compliant with respect to a functional or a safety requirement.<\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li><a href=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/10\/Formal-software-analysis-leaflet-October-2021.pdf\" target=\"_blank\" rel=\"noopener noreferrer\">Download formal analysis of software leaflet<\/a><\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<p>This approach establishes a direct formal link between the source code of the software and the properties of the system that integrates that software. It is now possible to detect any kind of noncompliance that may have been introduced in the design phase: from the identification of algorithms during the system definition phase, up to their concrete realization, taking into account possible implementation specific constraints.<\/p>\r\n\r\n\r\n\r\n<p><strong>The formal analysis approach proposed by CLEARSY is complete:<\/strong> it is guaranteed to cover all possible functional behaviors, including as a matter of fact all system dysfunctions and failures that have not explicitly been discarded. This is the benefit of using a method based on mathematics and a property-based approach, instead of a case-by-case approach.<\/p>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Industrial interest<\/h2>\r\n\r\n\r\n\r\n<p class=\"lanceur\">The benefits of such a formal analysis numerous:<\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li>\u00a0 To consolidate and lay down <strong>the functional and safety requirements:<\/strong> to state explicitly what guarantees the system shall enforce. \u00a0<\/li>\r\n<li>\u00a0 <strong>To identify non compliant behaviors:<\/strong> violations of properties that may have deep consequences on the safety or on the operation of the system integrating the software under analysis. \u00a0<\/li>\r\n<li>\u00a0 <strong>Recover initial reasonings:<\/strong> the original intentions of the system designers. \u00a0<\/li>\r\n<li>\u00a0 <strong>Lay down design choices:<\/strong> by finding their justification, thus providing a guarantee that the software under analysis is technically mastered. \u00a0<\/li>\r\n<li>\u00a0 <strong>Uncover useless or obsolete complexity nodes:<\/strong> to simplify the software for improved performance and functional features (the simpler the software, the larger the possibility to be well-behaved). \u00a0<\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Quickly providing concrete results<\/h2>\r\n\r\n\r\n\r\n<p class=\"lanceur\">This method is pragmatic, quickly providing concrete results for the project. With the results obtained from previous applications, CLEARSY has reached the conclusion that the formal analysis of software presents a real gain both for the supplier of a product and its operator.<\/p>\r\n\r\n\r\n\r\n<p>The approach benefits from being used on products that evolve over time, or that are widely deployed, or that integrate options based on their use.<\/p>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Commercial references<\/h2>\r\n<table style=\"border-collapse: collapse; width: 100%;\" border=\"1\">\r\n<tbody>\r\n<tr>\r\n<td style=\"width: 50%;\">\r\n<figure><img loading=\"lazy\" decoding=\"async\" width=\"326\" height=\"230\" src=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-Alstom.png\" alt=\"\" data-id=\"14919\" data-full-url=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-Alstom.png\" data-link=\"https:\/\/www.clearsy.com\/en\/tools\/data-solver\/logo-alstom-4-2\/\" class=\"wp-image-14919\" srcset=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-Alstom.png 326w, https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-Alstom-300x212.png 300w\" sizes=\"auto, (max-width: 326px) 100vw, 326px\" \/><\/figure>\r\n<\/td>\r\n<td style=\"width: 50%;\">\r\n<figure><img loading=\"lazy\" decoding=\"async\" width=\"326\" height=\"230\" src=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-RATP.png\" alt=\"\" data-id=\"14929\" data-full-url=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-RATP.png\" data-link=\"https:\/\/www.clearsy.com\/en\/tools\/data-solver\/logo-ratp-2-2\/\" class=\"wp-image-14929\" srcset=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-RATP.png 326w, https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-RATP-300x212.png 300w\" sizes=\"auto, (max-width: 326px) 100vw, 326px\" \/><\/figure>\r\n<\/td>\r\n<\/tr>\r\n<tr>\r\n<td style=\"width: 50%;\">\r\n<figure><img loading=\"lazy\" decoding=\"async\" width=\"326\" height=\"230\" src=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-SNCF-Reseau.png\" alt=\"\" data-id=\"14921\" data-full-url=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-SNCF-Reseau.png\" data-link=\"https:\/\/www.clearsy.com\/en\/tools\/data-solver\/logo-sncf-reseau-2\/\" class=\"wp-image-14921\" srcset=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-SNCF-Reseau.png 326w, https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-SNCF-Reseau-300x212.png 300w\" sizes=\"auto, (max-width: 326px) 100vw, 326px\" \/><\/figure>\r\n<\/td>\r\n<td style=\"width: 50%;\">\r\n<figure class=\"wp-block-gallery columns-4 is-cropped\">\r\n<figure><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-new-york-city-transit.png\" alt=\"New York City Transit\" data-id=\"14986\" data-full-url=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-new-york-city-transit.png\" data-link=\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/logo-new-york-city-transit-2\/\" class=\"wp-image-14986\" width=\"222\" height=\"157\" srcset=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-new-york-city-transit.png 326w, https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-new-york-city-transit-300x212.png 300w\" sizes=\"auto, (max-width: 222px) 100vw, 222px\" \/><\/figure>\r\n<\/figure>\r\n<\/td>\r\n<\/tr>\r\n<\/tbody>\r\n<\/table>\r\n\r\n\r\n","protected":false},"excerpt":{"rendered":"<p>CLEARSY proposes a new innovative analysis approach to establish with mathematical proof that all or part of a software are [&hellip;]<\/p>\n","protected":false},"featured_media":18437,"template":"","domaine":[499],"class_list":["post-14796","offres","type-offres","status-publish","has-post-thumbnail","hentry","domaine-railway"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.1.1 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Formal analysis and validation of software - 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-analysis-of-software\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Formal analysis and validation of software - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"CLEARSY proposes a new innovative analysis approach to establish with mathematical proof that all or part of a software are [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:modified_time\" content=\"2022-04-14T16:12:52+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png\" \/>\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\/png\" \/>\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=\"3 minutes\" \/>\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-analysis-of-software\/\",\"url\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/\",\"name\":\"Formal analysis and validation of software - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png\",\"datePublished\":\"2020-07-24T12:54:02+00:00\",\"dateModified\":\"2022-04-14T16:12:52+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage\",\"url\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png\",\"contentUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png\",\"width\":1170,\"height\":615},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#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 analysis and validation of software\"}]},{\"@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 analysis and validation of software - 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-analysis-of-software\/","og_locale":"en_US","og_type":"article","og_title":"Formal analysis and validation of software - CLEARSY","og_description":"CLEARSY proposes a new innovative analysis approach to establish with mathematical proof that all or part of a software are [&hellip;]","og_url":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/","og_site_name":"CLEARSY","article_modified_time":"2022-04-14T16:12:52+00:00","og_image":[{"width":1170,"height":615,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png","type":"image\/png"}],"twitter_card":"summary_large_image","twitter_misc":{"Est. reading time":"3 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/","url":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/","name":"Formal analysis and validation of software - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png","datePublished":"2020-07-24T12:54:02+00:00","dateModified":"2022-04-14T16:12:52+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/analyse-logiciel-us-1-1.png","width":1170,"height":615},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/offers\/formal-analysis-of-software\/#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 analysis and validation of software"}]},{"@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\/14796","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\/14796\/revisions"}],"predecessor-version":[{"id":18034,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/offres\/14796\/revisions\/18034"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/18437"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=14796"}],"wp:term":[{"taxonomy":"domaine","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/domaine?post=14796"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}