{"id":1692,"date":"2020-11-19T10:15:45","date_gmt":"2020-11-19T09:15:45","guid":{"rendered":"https:\/\/www.systerel.fr\/en\/?p=1692"},"modified":"2023-03-24T15:01:01","modified_gmt":"2023-03-24T14:01:01","slug":"spark_ada","status":"publish","type":"post","link":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/","title":{"rendered":"SPARK\/Ada"},"content":{"rendered":"\n

Systerel implements a formal verification approach through SPARK\/Ada.<\/strong><\/p>\n\n\n\n

Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC.<\/p>\n\n\n\n

The objectives to be achieved on these legacy codes are to verify that:<\/p>\n\n\n\n

1. The data flow is in agreement with the information provided.<\/p>\n\n\n\n

2. The semantics of the operations are in agreement with the available or expressed semantics.<\/p>\n\n\n\n

3. The code does not raise exceptions (AoRTE).<\/p>\n\n\n\n

This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting.<\/p>\n\n\n\n

But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012.<\/p>\n\n\n\n

Its implementation is then simplified and can be done with a reasonable learning curve.<\/p>\n\n\n\n

The adoption of SPARK will then contribute in the long term:<\/p>\n\n\n\n

1. To structural quality,<\/p>\n\n\n\n

2.  To functional quality,<\/p>\n\n\n\n

3.  To maintainability (Contracts –> test oracles),<\/p>\n\n\n\n

4. To the satisfaction of the Safety and Security requirements,<\/p>\n\n\n\n

5. As a “technical” aestheticism.<\/p>\n\n\nOur Ada Expertise<\/a>\n","protected":false},"excerpt":{"rendered":"

Systerel uses SPARK\/Ada formal verification technology in developments for its customers in the railway sector (EN 50128 standard).<\/p>\n","protected":false},"author":19,"featured_media":1694,"comment_status":"closed","ping_status":"closed","sticky":true,"template":"","format":"standard","meta":{"footnotes":""},"categories":[14],"tags":[],"class_list":["post-1692","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-formal-methods"],"yoast_head":"\nSPARK\/Ada<\/title>\n<meta name=\"description\" content=\"Systerel implements a formal verification approach through SPARK\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a "technical" aestheticism.\" \/>\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\/news\/spark_ada\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"SPARK\/Ada\" \/>\n<meta property=\"og:description\" content=\"Systerel implements a formal verification approach through SPARK\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a "technical" aestheticism.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/\" \/>\n<meta property=\"og:site_name\" content=\"Systerel English\" \/>\n<meta property=\"article:published_time\" content=\"2020-11-19T09:15:45+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2023-03-24T14:01:01+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png\" \/>\n\t<meta property=\"og:image:width\" content=\"590\" \/>\n\t<meta property=\"og:image:height\" content=\"393\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/png\" \/>\n<meta name=\"author\" content=\"coralie\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"coralie\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/\"},\"author\":{\"name\":\"coralie\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\"},\"headline\":\"SPARK\\\/Ada\",\"datePublished\":\"2020-11-19T09:15:45+00:00\",\"dateModified\":\"2023-03-24T14:01:01+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/\"},\"wordCount\":199,\"image\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2020\\\/11\\\/Spark_590.png\",\"articleSection\":[\"Formal Methods\"],\"inLanguage\":\"en-US\"},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/\",\"name\":\"SPARK\\\/Ada\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2020\\\/11\\\/Spark_590.png\",\"datePublished\":\"2020-11-19T09:15:45+00:00\",\"dateModified\":\"2023-03-24T14:01:01+00:00\",\"author\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\"},\"description\":\"Systerel implements a formal verification approach through SPARK\\\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\\\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a \\\"technical\\\" aestheticism.\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#primaryimage\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2020\\\/11\\\/Spark_590.png\",\"contentUrl\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2020\\\/11\\\/Spark_590.png\",\"width\":590,\"height\":393,\"caption\":\"SPARK\\\/Ada\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/spark_ada\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"SPARK\\\/Ada\"}]},{\"@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\"},{\"@type\":\"Person\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\",\"name\":\"coralie\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"caption\":\"coralie\"},\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/author\\\/coralie\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"SPARK\/Ada","description":"Systerel implements a formal verification approach through SPARK\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a \"technical\" aestheticism.","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\/news\/spark_ada\/","og_locale":"en_US","og_type":"article","og_title":"SPARK\/Ada","og_description":"Systerel implements a formal verification approach through SPARK\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a \"technical\" aestheticism.","og_url":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/","og_site_name":"Systerel English","article_published_time":"2020-11-19T09:15:45+00:00","article_modified_time":"2023-03-24T14:01:01+00:00","og_image":[{"width":590,"height":393,"url":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png","type":"image\/png"}],"author":"coralie","twitter_misc":{"Written by":"coralie","Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#article","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/"},"author":{"name":"coralie","@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db"},"headline":"SPARK\/Ada","datePublished":"2020-11-19T09:15:45+00:00","dateModified":"2023-03-24T14:01:01+00:00","mainEntityOfPage":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/"},"wordCount":199,"image":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#primaryimage"},"thumbnailUrl":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png","articleSection":["Formal Methods"],"inLanguage":"en-US"},{"@type":"WebPage","@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/","url":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/","name":"SPARK\/Ada","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#primaryimage"},"image":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#primaryimage"},"thumbnailUrl":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png","datePublished":"2020-11-19T09:15:45+00:00","dateModified":"2023-03-24T14:01:01+00:00","author":{"@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db"},"description":"Systerel implements a formal verification approach through SPARK\/Ada. Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC. The objectives to be achieved on these legacy codes are to verify that: 1. The data flow is in agreement with the information provided. 2. The semantics of the operations are in agreement with the available or expressed semantics. 3. The code does not raise exceptions (AoRTE). This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting. But SPARK\/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012. Its implementation is then simplified and can be done with a reasonable learning curve. The adoption of SPARK will then contribute in the long term: 1. To structural quality, 2. To functional quality, 3. To maintainability (Contracts --> test oracles), 4. To the satisfaction of the Safety and Security requirements, 5. as a \"technical\" aestheticism.","breadcrumb":{"@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.systerel.fr\/en\/news\/spark_ada\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#primaryimage","url":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png","contentUrl":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2020\/11\/Spark_590.png","width":590,"height":393,"caption":"SPARK\/Ada"},{"@type":"BreadcrumbList","@id":"https:\/\/www.systerel.fr\/en\/news\/spark_ada\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.systerel.fr\/en\/"},{"@type":"ListItem","position":2,"name":"SPARK\/Ada"}]},{"@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"},{"@type":"Person","@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db","name":"coralie","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","caption":"coralie"},"url":"https:\/\/www.systerel.fr\/en\/news\/author\/coralie\/"}]}},"_links":{"self":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/1692","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/users\/19"}],"replies":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/comments?post=1692"}],"version-history":[{"count":4,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/1692\/revisions"}],"predecessor-version":[{"id":1717,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/1692\/revisions\/1717"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media\/1694"}],"wp:attachment":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media?parent=1692"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/categories?post=1692"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/tags?post=1692"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}