Autoria: Aryldo G. Russo Júnior – Consultor
Este artigo propõe uma ferramenta gráfica baseada em métodos formais para validar as condições topológicas das vias e as condições de movimentação de trens. Esta ferramenta está baseada no Eclipse e incorporada à plataforma Rodin. Suas principais características estão resumidas na simulação gráfica das especificações da sinalização de ferrovias e na validação das propriedades da movimentação dos trens. A fase de validação, que é crítica, é feita usualmente de forma manual, o que representa um risco potencial para a segurança dos passageiros se não for feita corretamente. A ferramenta é chamada VeRaSiS e utiliza a linguagem Event-B para formalizar, provar e verificar estas propriedades de forma automática.
http://www.aeamesp.org.br/biblioteca/stm/17smtf110916t4301.pdf