Metodologia de geração automática de testes via Model Checking guiada por critério de cobertura MC/DC para validação de sistemas críticos de automação naval

Abstract

Sistemas Críticos de Automação (SCAs) em aplicações de alto risco, como as do setor naval, demandam alta confiabilidade, uma vez que falhas no software de controle podem acarretar consequências catastróficas. Contudo, a validação manual de códigos para Controladores Lógicos Programáveis (CLPs) mostra-se onerosa, sujeita a erros humanos e limitada na cobertura de cenários. Inserida em um ciclo de desenvolvimento assistido por Model Checking (MC), esta dissertação apresenta uma metodologia para a geração automática de casos de teste e oráculos direcionada a SCA navais utilizando teste baseado em MC. O objetivo principal consiste em reutilizar os modelos abstratos da fase de verificação para conceber o plano de testes da etapa de validação. Para tanto, a abordagem utiliza padrões da indústria, como a Matriz de Causa e Efeito (MCE) e o GRAFCET para modelar especificações funcionais e comportamentos sequenciais temporizados. A extração dos casos de teste parte do modelo abstrato traduzido diretamente do Diagrama Lógico Binário (DLB), utilizando a linguagem formal intermediária FIACRE para gerar um Sistema de Transição Temporizado (TTS). Em seguida, a metodologia emprega Diagramas de Decisão Binária (BDD) para extrair os caminhos lógicos que satisfazem o critério de Cobertura Modificada de Condições/Decisões (MC/DC), traduzindo-os sistematicamente em propriedades-armadilha expressas em Lógica Temporal Linear (LTL). Na etapa de verificação, utilizam-se as ferramentas do TINA por meio da técnica de On-the-Fly MC, visando mitigar a explosão de estados e garantir caminhos mais curtos de teste, cujos contraexemplos gerados são reinterpretados como casos de teste. A metodologia foi validada por meio de um estudo de caso do sistema de controle de partida e parada de um motor, implementado em um CLP físico em ambiente de laboratório. O conjunto de testes gerado foi capaz de detectar erros induzidos nas lógicas implementadas no ladder do CLP, demonstrando que a abordagem extrai cenários de teste factíveis que cobrem tanto a ativação quanto a desativação de saídas, estados e transições a partir de cada causa independentemente. A limitação do método, intrínseca a abordagens de caixa-preta, reside na detecção de códigos ocultos não previstos nas funções de ativação originais. Por fim, a estratégia proposta garante uma cobertura satisfatória com baixo custo computacional e de teste, complementando testes manuais e elevando o nível de segurança no ciclo de desenvolvimento de sistemas de automação.

Abstract: Critical Automation Systems (CAS) in high-risk applications, such as in the naval domain, demand high reliability, given that failures in control software can lead to catastrophic consequences. Manual code validation for Programmable Logic Controllers (PLCs) proves to be resource-intensive, error-prone, and limited in scenario coverage. Integrated into a development lifecycle assisted by Model Checking (MC), this dissertation proposes a methodology for the automated generation of test cases and oracles tailored to naval CAS using MC-based testing. The primary objective is to reuse abstract models from the verification phase to design the test plan for the validation phase. To this end, the approach employs industry standards such as the Cause and Effect Matrix (CEM) and GRAFCET to model functional specifications and timed sequential behaviors. Test case extraction from the abstract model translated directly from the Binary Logic Diagram (BLD), utilizing the FIACRE intermediate formal language to generate a Timed Transition System (TTS). Subsequently, the methodology applies Binary Decision Diagrams (BDD) to extract the logical execution paths that satisfy the Modified Condition/Decision Coverage (MC/DC) criterion, systematically translating them into trap properties expressed in Linear Temporal Logic (LTL). In the verification phase, the capabilities of the TINA toolset are leveraged via On-the-Fly MC to mitigate state-space explosion and ensure minimal-length test paths, whose generated counterexamples are reinterpreted as test cases. The methodology was validated through a case study on a motor start and stop control system implemented on a physical PLC in a laboratory environment. The generated test suite successfully detected injected errors in the PLC ladder logic, demonstrating that the approach extracts feasible test scenarios that cover both activation and deactivation of outputs, states, and transitions independently for each cause. A limitation of the method, intrinsic to black-box testing approaches, lies in the detection of hidden code not accounted for in the original activation functions. Finally, the proposed strategy ensures satisfactory coverage with low computational and testing effort, complementing manual testing and enhancing the safety level throughout the automation system development lifecycle.