{"id":317,"date":"2014-09-25T15:23:15","date_gmt":"2014-09-25T14:23:15","guid":{"rendered":"http:\/\/www.systerel.fr\/en\/?page_id=317"},"modified":"2026-04-15T17:14:07","modified_gmt":"2026-04-15T16:14:07","slug":"rodin-platform","status":"publish","type":"page","link":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/","title":{"rendered":"Rodin Platform"},"content":{"rendered":"\n<p><strong>Systerel is the technical leader of the Rodin platform<\/strong>, ensuring its maintenance and ongoing evolution.<br>The activities developed around the platform enable us to consolidate and further develop our expertise in the Eclipse ecosystem and in Event-B modeling.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">What is the Rodin Platform?<\/h2>\n\n\n\n<p>The Rodin platform is the dedicated tool for Event-B modelling, robustly supporting model refinement and mathematical proof.<\/p>\n\n\n\n<p>It was created in Zurich as part of the European FP7 project of the same name between 2004 and 2007. Systerel led its corrective and evolutionary maintenance from 2007 to 2025. Since then, maintenance has been carried out by IRIT and CentraleSup\u00e9lec. It is an open-source platform based on the Eclipse IDE.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Use cases at Systerel<\/h2>\n\n\n\n<p>Formal modeling and proof of the safety of systems, such as:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>RATP Directive 41 for metro interlockings<\/li>\n\n\n\n<li>CBTC metro trackside systems<\/li>\n\n\n\n<li>HELISAR helicopter hoist system<\/li>\n<\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">ABZ conference and Rodin workshop<\/h2>\n\n\n\n<p>Systerel is a member of the program committee of the <a href=\"https:\/\/abz-conf.org\/\" target=\"_blank\" rel=\"noreferrer noopener\">ABZ conferences<\/a>, which are dedicated to the cross-fertilization of several formal methods, linked by their state-based and machine-based approaches: Abstract State Machines (ASM), Alloy, Classical B, Event-B, Temporal Logic of Actions (TLA), Vienna Development Method (VDM), and the Z notation.<\/p>\n\n\n\n<p>Systerel has participated in the organization of all \u201c<a href=\"https:\/\/wiki.event-b.org\/index.php\/Main_Page\" target=\"_blank\" rel=\"noreferrer noopener\">RODIN User and Developer Workshop<\/a>\u201d events.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Publications<\/h2>\n\n\n\n<p>Systerel actively contributes to the dissemination of work carried out around the Rodin platform and formal methods.<\/p>\n\n\n\n<p>Our teams regularly publish in leading international conferences and workshops, sharing feedback, methodological advances, and technical contributions.<\/p>\n\n\n\n<p><strong><a href=\"https:\/\/blog.systerel.fr\/pages\/publications\/\">All of our publications are available on our blog.<\/a><\/strong><\/p>\n\n\n\n<p class=\"SYSNormal\"><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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","protected":false},"author":1,"featured_media":0,"parent":305,"menu_order":5,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-317","page","type-page","status-publish","hentry"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.4 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Rodin Platform - Systerel English<\/title>\n<meta name=\"description\" content=\"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.\" \/>\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\/rodin-platform\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Rodin Platform - Systerel English\" \/>\n<meta property=\"og:description\" content=\"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/\" \/>\n<meta property=\"og:site_name\" content=\"Systerel English\" \/>\n<meta property=\"article:modified_time\" content=\"2026-04-15T16:14:07+00:00\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"2 minutes\" \/>\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\\\/rodin-platform\\\/\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/rodin-platform\\\/\",\"name\":\"Rodin Platform - Systerel English\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\"},\"datePublished\":\"2014-09-25T14:23:15+00:00\",\"dateModified\":\"2026-04-15T16:14:07+00:00\",\"description\":\"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/rodin-platform\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/rodin-platform\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/rodin-platform\\\/#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\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/expertise\\\/formal-methods\\\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"Rodin Platform\"}]},{\"@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":"Rodin Platform - Systerel English","description":"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.","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\/rodin-platform\/","og_locale":"en_US","og_type":"article","og_title":"Rodin Platform - Systerel English","og_description":"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.","og_url":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/","og_site_name":"Systerel English","article_modified_time":"2026-04-15T16:14:07+00:00","twitter_misc":{"Est. reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/","url":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/","name":"Rodin Platform - Systerel English","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/#website"},"datePublished":"2014-09-25T14:23:15+00:00","dateModified":"2026-04-15T16:14:07+00:00","description":"Systerel is the technical leader of the Rodin platform, a dedicated tool for Event-B development, supporting model refinement and mathematical proof.","breadcrumb":{"@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/rodin-platform\/#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","item":"https:\/\/www.systerel.fr\/en\/expertise\/formal-methods\/"},{"@type":"ListItem","position":4,"name":"Rodin Platform"}]},{"@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\/317","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=317"}],"version-history":[{"count":16,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/317\/revisions"}],"predecessor-version":[{"id":3869,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/317\/revisions\/3869"}],"up":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/305"}],"wp:attachment":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media?parent=317"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}