{"id":305,"date":"2014-09-25T15:08:46","date_gmt":"2014-09-25T14:08:46","guid":{"rendered":"http:\/\/www.systerel.fr\/en\/?page_id=305"},"modified":"2025-11-13T17:45:51","modified_gmt":"2025-11-13T16:45:51","slug":"formal-methods","status":"publish","type":"page","link":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/","title":{"rendered":"Formal methods"},"content":{"rendered":"

Systerel\u2019s ‘Formal Modeling and Verification’ Center of Expertise is one of the largest European teams in this field and has over 25 years of experience in the industrial implementation of formal methods.<\/p>\n\n\t

\n\t\t
\n\n\t\t\t\n\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Use of Formal Methods<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Why use formal methods?
\nWhich techniques for which challenges?<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t\t\t\n\t\t\t\t\t

\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Model Checking with S3<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel uses Model Checking to verify the safety properties of artifacts in the system development process. It relies on models\/translations in HLL and on the S3 proof engine.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t\t\t\n\t\t\t\t\t

\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

B Method Software<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel uses the formal B method for the development of safety-critical software in an industrial context. This technique allows for proving that the software\u2019s formal specification is consistent and that its code conforms to the specification<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t<\/div>

\n\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Data Verification with B OVADO\u00b2\u00ae<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel uses the formal method B OVADO\u00b2\u00ae to validate the configuration data of a system. This technique is based on verifying the compliance of each data set with predefined rules using the OVADO\u00b2\u00ae tool from RATP.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t\t\t\n\t\t\t\t\t

\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Rodin Platform<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel uses the formal Event-B method to prove that a system meets safety properties. This technique relies on the RODIN platform, which Systerel maintains and develops further.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t\t\t\n\t\t\t\t\t

\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

SCADE Modeling<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel provides consulting and expertise services related to the implementation of SCADE and its integration with other technologies.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t<\/div>

\n\t\t\t\t\n\t\t\t\t\t
\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

HLL Language<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel has now been using HLL for many years in the formal safety verification of critical systems such as CBTCs, interlockings, logical control-command circuits, but also for the optimization of constrained systems.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t\t\t\n\t\t\t\t\t

\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Verification & Validation Tools<\/h4>\n\t\t\t\t\t\t<\/header>\n\t\t\t\t\t\t
\n\t\t\t\t\t\t\t

Systerel develops solutions using formal methods to increase quality and productivity in the areas of verification and validation.<\/p>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/a>\n\n\t\t\t\t\n\t\t<\/div>\n\t<\/section>\n\n\t\n","protected":false},"excerpt":{"rendered":"

Systerel\u2019s expert center \u201cModeling and proof\u201d consists of one of Europe\u2019s most important teams in the field.<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":303,"menu_order":1,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-305","page","type-page","status-publish","hentry"],"yoast_head":"\nFormal methods - Systerel English<\/title>\n<meta name=\"description\" content=\"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.\" \/>\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.systerel.fr\/en\/expertise\/formal-methods\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Formal methods - Systerel English\" \/>\n<meta property=\"og:description\" content=\"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/\" \/>\n<meta property=\"og:site_name\" content=\"Systerel English\" \/>\n<meta property=\"article:modified_time\" content=\"2025-11-13T16:45:51+00:00\" \/>\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.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/\",\"name\":\"Formal methods - Systerel English\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\"},\"datePublished\":\"2014-09-25T14:08:46+00:00\",\"dateModified\":\"2025-11-13T16:45:51+00:00\",\"description\":\"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Expertise\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Formal methods\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\",\"name\":\"Systerel English\",\"description\":\"Safe real-time solutions\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Formal methods - Systerel English","description":"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.","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.systerel.fr\/en\/expertise\/formal-methods\/","og_locale":"en_US","og_type":"article","og_title":"Formal methods - Systerel English","og_description":"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.","og_url":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/","og_site_name":"Systerel English","article_modified_time":"2025-11-13T16:45:51+00:00","twitter_misc":{"Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/","url":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/","name":"Formal methods - Systerel English","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/#website"},"datePublished":"2014-09-25T14:08:46+00:00","dateModified":"2025-11-13T16:45:51+00:00","description":"Systerel\u2019s 'Formal Modeling and Verification' Center of Expertise is one of the largest European teams in formal methods.","breadcrumb":{"@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.systerel.fr\/en\/"},{"@type":"ListItem","position":2,"name":"Expertise","item":"https:\/\/www.systerel.fr\/en\/expertise\/"},{"@type":"ListItem","position":3,"name":"Formal methods"}]},{"@type":"WebSite","@id":"https:\/\/www.systerel.fr\/en\/#website","url":"https:\/\/www.systerel.fr\/en\/","name":"Systerel English","description":"Safe real-time solutions","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.systerel.fr\/en\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"}]}},"_links":{"self":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/305","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/comments?post=305"}],"version-history":[{"count":12,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/305\/revisions"}],"predecessor-version":[{"id":3592,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/305\/revisions\/3592"}],"up":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/303"}],"wp:attachment":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media?parent=305"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}