{"id":1701,"date":"2011-12-13T21:12:13","date_gmt":"1899-12-30T00:00:00","guid":{"rendered":"https:\/\/aeamesp.org.br\/site2025\/abordagem-formal-da-verificacao-dos-sistemas-de-sinalizacao-de-trens-usando-a-linguagem-event-b\/"},"modified":"2011-12-13T21:12:13","modified_gmt":"1899-12-30T00:00:00","slug":"abordagem-formal-da-verificacao-dos-sistemas-de-sinalizacao-de-trens-usando-a-linguagem-event-b","status":"publish","type":"post","link":"https:\/\/aeamesp.org.br\/site2025\/abordagem-formal-da-verificacao-dos-sistemas-de-sinalizacao-de-trens-usando-a-linguagem-event-b\/","title":{"rendered":"Abordagem formal da verifica\u00e7\u00e3o dos sistemas de sinaliza\u00e7\u00e3o de trens usando a Linguagem Event-B"},"content":{"rendered":"<p><strong>Autoria: Aryldo G. Russo J\u00fanior &#8211; Consultor<\/strong><\/p>\n<hr \/>\n<p style=\"text-align: justify;\"><strong>\u00a0 \u00a0Este artigo prop\u00f5e uma ferramenta gr\u00e1fica baseada em m\u00e9todos formais para validar as condi\u00e7\u00f5es topol\u00f3gicas das vias e as condi\u00e7\u00f5es de movimenta\u00e7\u00e3o de trens. Esta ferramenta est\u00e1 baseada no Eclipse e incorporada \u00e0 plataforma Rodin. Suas principais caracter\u00edsticas est\u00e3o resumidas na simula\u00e7\u00e3o gr\u00e1fica das especifica\u00e7\u00f5es da sinaliza\u00e7\u00e3o de ferrovias e na valida\u00e7\u00e3o das propriedades da movimenta\u00e7\u00e3o dos trens. A fase de valida\u00e7\u00e3o, que \u00e9 cr\u00edtica, \u00e9 feita usualmente de forma manual, o que representa um risco potencial para a seguran\u00e7a dos passageiros se n\u00e3o for feita corretamente. A ferramenta \u00e9 chamada VeRaSiS e utiliza a linguagem Event-B para formalizar, provar e verificar estas propriedades de forma autom\u00e1tica.<\/strong><\/p>\n<hr \/>\n<p style=\"text-align: justify;\"><a href=\"http:\/\/www.aeamesp.org.br\/biblioteca\/stm\/17smtf110916t4301.pdf\" target=\"_blank\">http:\/\/www.aeamesp.org.br\/biblioteca\/stm\/17smtf110916t4301.pdf<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Autoria: Aryldo G. Russo J\u00fanior &#8211; Consultor \u00a0 \u00a0Este artigo&hellip;<\/p>\n<p> <a class=\"more-link\" href=\"https:\/\/aeamesp.org.br\/site2025\/abordagem-formal-da-verificacao-dos-sistemas-de-sinalizacao-de-trens-usando-a-linguagem-event-b\/\">Leia mais<\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"pagelayer_contact_templates":[],"_pagelayer_content":"","_kadence_starter_templates_imported_post":false,"footnotes":""},"categories":[37],"tags":[],"class_list":{"0":"post-1701","1":"post","2":"type-post","3":"status-publish","4":"format-standard","6":"category-17a-semana-de-tecnologia-metroferroviaria"},"_links":{"self":[{"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/posts\/1701","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/comments?post=1701"}],"version-history":[{"count":0,"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/posts\/1701\/revisions"}],"wp:attachment":[{"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/media?parent=1701"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/categories?post=1701"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/aeamesp.org.br\/site2025\/wp-json\/wp\/v2\/tags?post=1701"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}