{"id":12782,"date":"2020-07-10T17:07:07","date_gmt":"2020-07-10T15:07:07","guid":{"rendered":"http:\/\/localhost:8888\/clearsy\/?post_type=thematiques&p=12782"},"modified":"2025-11-14T10:26:35","modified_gmt":"2025-11-14T08:26:35","slug":"b-method","status":"publish","type":"thematiques","link":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/","title":{"rendered":"B method"},"content":{"rendered":"\r\n

The B METHOD<\/a> is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, by means of mathematical proofs, in order to prove their data consistency. This process is especially useful for removing any ambiguity in the properties initially expressed in natural language.<\/p>\r\n\r\n\r\n\r\n

The B language can be used in protocols as well as in embedded computing. Moreover, the B method encompasses all modelling by the proof of a system, from the writing of its model to the installation of its software.<\/p>\r\n\r\n\r\n\r\n

Although the uses of the B method are diverse (modelling of a system, formalisation of specifications \u2026) the aim is the same: to use mathematical proofs to ensure the reliability and security of a system and to make sure that there are no computer bugs in the system.<\/p>\r\n\r\n\r\n\r\n

The B method draws its legitimacy from the development of approved tools, which are used on a large scale both in the world of industry and in the university sphere, such as Atelier B. CLEARSY is the holder of Atelier B and is responsible for its development and for the maintenance of its development platform. Atelier B<\/a> therefore constitutes a reference for the development of proven software.<\/p>\r\n\r\n\r\n\r\n

\"Teaching\r\n
Learning B in France<\/figcaption>\r\n<\/figure>\r\n\r\n\r\n\r\n

Formal verification of specifications<\/h2>\r\n\r\n\r\n\r\n

Due to our experience in modeling and our ability to understand and abstract our clients\u2019 needs, we are able to support operators, industry and originators in verifying specifications for systems and software.<\/p>\r\n\r\n\r\n\r\n

The B Method, associated with other formalisms, is used to analyze, validate, reorganize and provide elements that may complete specifications.<\/p>\r\n\r\n\r\n\r\n

This approach is applicable to every industrial sector. Today, it is used successfully in the automotive, bank, space and nuclear sectors.<\/p>\r\n\r\n\r\n\r\n

Advantages of the formal verification<\/h3>\r\n\r\n\r\n\r\n

The advantages observed are :<\/p>\r\n\r\n\r\n\r\n

    \r\n
  • A more rapid focus on difficult areas<\/li>\r\n
  • Reliable and justifiable summary<\/li>\r\n
  • Direct and precise questionning<\/li>\r\n
  • Proof of coherence<\/li>\r\n
  • Achievable completeness<\/li>\r\n
  • Elimination of professional \u201cunsaids requirements\u201d<\/li>\r\n
  • Consideration of functional and dysfunctional aspects<\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n

    For a return on investment that is positive in terms of:<\/p>\r\n\r\n\r\n\r\n

      \r\n
    • Decrease iin delayed features<\/li>\r\n
    • Gains in validation (Improved testability)<\/li>\r\n
    • More rapid convergence (Realization quality)<\/li>\r\n
    • Greater capitalization of knowledge<\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n
      \"ATELIER<\/figure>\r\n","protected":false},"excerpt":{"rendered":"

      The B METHOD is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, […]<\/p>\n","protected":false},"featured_media":16887,"parent":0,"template":"","domaine":[],"class_list":["post-12782","thematiques","type-thematiques","status-publish","has-post-thumbnail","hentry"],"acf":[],"yoast_head":"\nB method - 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\/thematics\/b-method\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"B method - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"The B METHOD is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, […]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:modified_time\" content=\"2025-11-14T08:26:35+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"2560\" \/>\n\t<meta property=\"og:image:height\" content=\"1342\" \/>\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=\"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\/thematics\/b-method\/\",\"url\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/\",\"name\":\"B method - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg\",\"datePublished\":\"2020-07-10T15:07:07+00:00\",\"dateModified\":\"2025-11-14T08:26:35+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage\",\"url\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg\",\"contentUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg\",\"width\":2560,\"height\":1342},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.clearsy.com\/en\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Thematic\",\"item\":\"https:\/\/www.clearsy.com\/en\/thematics\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"B method\"}]},{\"@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":"B method - 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\/thematics\/b-method\/","og_locale":"en_US","og_type":"article","og_title":"B method - CLEARSY","og_description":"The B METHOD is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, […]","og_url":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/","og_site_name":"CLEARSY","article_modified_time":"2025-11-14T08:26:35+00:00","og_image":[{"width":2560,"height":1342,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg","type":"image\/jpeg"}],"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\/thematics\/b-method\/","url":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/","name":"B method - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg","datePublished":"2020-07-10T15:07:07+00:00","dateModified":"2025-11-14T08:26:35+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/thematics\/b-method\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/07\/logo-mtb-en-scaled.jpg","width":2560,"height":1342},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/thematics\/b-method\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"Thematic","item":"https:\/\/www.clearsy.com\/en\/thematics\/"},{"@type":"ListItem","position":3,"name":"B method"}]},{"@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\/thematiques\/12782","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/thematiques"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/thematiques"}],"version-history":[{"count":5,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/thematiques\/12782\/revisions"}],"predecessor-version":[{"id":20874,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/thematiques\/12782\/revisions\/20874"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/16887"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=12782"}],"wp:term":[{"taxonomy":"domaine","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/domaine?post=12782"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}