Metodologia para desenvolvimento de sistemas de controle e monitoração de navios assistido por model checking

Abstract

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.

Abstract : The Brazilian Navy develops the Control and Monitoring System for several ships in its fleet. This system is responsible for controlling the ship's main and auxiliary engines and is essential for its operation and safety. This work proposes a project development methodology for the Brazilian Navy Control and Monitoring System, using formal verification by model checking. The methodology establishes specification documents and translation methods for the language interpreted by the formal verification tool. Thus, making it possible to certify in an exhaustive and automatic way that all the essential safe properties to the project are included in the code specification document for the Programmable Logic Controller (PLC), generating cost reduction in error correction, and increasing reliability and availability of the ship. Because it is automatic, the method eliminates the need for designers to have formal verification skills. A typical Brazilian Navy s case study was used and confirmed the feasibility and efficacy of the proposed methodology.