Metodologia para desenvolvimento de sistemas de controle e monitoração de navios assistido por Model Checking

Abstract

The Brazilian Navy develops the Control and Monitoring System for several ships in it s 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 Co ntrol 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 ex haustive and aut omatic 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 reliabilit y and avai lability 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.