METODOLOGIA PARA DESENVOLVIMENTO DE SISTEMAS DE CONTROLE E MONITORAÇÃO DE NAVIOS ASSISTIDO POR MODEL CHECKING
Felipe da Silva Lázaro1; Max Hering de Queiroz2; Jean-Marie Farines2
1 Marinha do Brasil; 2 Universidade Federal de Santa Catarina
Baixar PDF doi:10.20906/CPS/CBA2018-0172
Resumo
A Marinha do Brasil (MB) desenvolve o Sistema de Controle e Monitoração (SCM) para diversos navios de sua esquadra. Este sistema é responsável pelo controle das máquinas principais e auxiliares do navio, sendo essencial para sua operação e segurança. Neste trabalho é proposta uma metodologia de desenvolvimento de projetos para o SCM da MB, utilizando verificação formal por model checking. A metodologia estabelece documentos de especificação e métodos de tradução para a linguagem interpretada pela ferramenta de verificação formal. Assim, possibilitando certificar, de forma exaustiva e automática, que todas as propriedades de segurança essenciais ao projeto estão constando no documento de especificação do código para o Controlador Lógico Programável (CLP), gerando redução de custos na correção de erros, e aumentando a confiabilidade e disponibilidade do navio. Por ser automático, o método dispensa a necessidade dos projetistas terem conhecimentos em verificação formal. Um estudo de caso típico da MB foi utilizado e confirmou a viabilidade e eficácia da metodologia proposta.
Palavras-chave: Model Checking; FIACRE; Verificação formal; Navios; Diagramas de lógica binária