{"id":812,"date":"2009-08-09T14:32:00","date_gmt":"2009-08-09T14:32:00","guid":{"rendered":"https:\/\/es-wordpress.fbk.eu\/?p=812"},"modified":"2021-05-10T10:06:41","modified_gmt":"2021-05-10T09:06:41","slug":"velos","status":"publish","type":"post","link":"https:\/\/es.fbk.eu\/index.php\/projects\/velos\/","title":{"rendered":"VELOS – Verifica Logica di Sicurezza"},"content":{"rendered":"\n[et_pb_section fb_built=”1″ admin_label=”section” _builder_version=”3.22″][et_pb_row admin_label=”row” _builder_version=”3.25″ background_size=”initial” background_position=”top_left” background_repeat=”repeat”][et_pb_column type=”4_4″ _builder_version=”3.25″ custom_padding=”|||” custom_padding__hover=”|||”][et_pb_text admin_label=”Text” _builder_version=”3.27.4″ background_size=”initial” background_position=”top_left” background_repeat=”repeat”]\n

Velos (Verifica Logica di Sicurezza) is a project aimed to apply formal methods to verification and validation of Logica di Sicurezza (LdS), software designed to monitor and control railway systems.<\/p>\n\n\n\n

VELOS is able to convert LdS specifications from a C++ like format to C and SMV. After this step several different tools can be used to validate the code. Depending on the user intention some of the generated SMV files can be merged into one and provided to NUSMV model checker which can verify the properties.<\/p>\n[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]\n","protected":false},"excerpt":{"rendered":"

Velos (Verifica Logica di Sicurezza) is a project aimed to apply formal methods to verification and validation of Logica di Sicurezza (LdS), software designed to monitor and control railway systems.<\/p>\n","protected":false},"author":1,"featured_media":819,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"\n

Velos (Verifica Logica di Sicurezza) is a project aimed to apply formal methods to verification and validation of Logica di Sicurezza (LdS), software designed to monitor and control railway systems.<\/p>\n\n\n\n

VELOS is able to convert LdS specifications from a C++ like format to C and SMV. After this step several different tools can be used to validate the code. Depending on the user intention some of the generated SMV files can be merged into one and provided to NUSMV model checker which can verify the properties.<\/p>\n","_et_gb_content_width":"","footnotes":""},"categories":[3],"tags":[],"class_list":["post-812","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-projects","et-has-post-format-content","et_post_format-et-post-format-standard"],"_links":{"self":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/812","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/comments?post=812"}],"version-history":[{"count":13,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/812\/revisions"}],"predecessor-version":[{"id":7066,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/812\/revisions\/7066"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media\/819"}],"wp:attachment":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media?parent=812"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/categories?post=812"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/tags?post=812"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}