Pós-Graduação em Ciência da Computação – UFPE
Defesa de Tese de Doutorado Nº 596
Aluno: Hugo Leonardo da Silva Araujo
Orientador: Prof. Augusto Alves Cezar Sampaio
Coorientador: Prof. Gustavo Henrique Porto de Carvalho
Título: A framework for testing cyber-physical systems: input generation
and causal analysis
Data: 23/03/2023
Hora/Local: 14h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinado
Prof. Nelson Souto Rosa (UFPE / Centro de Informática)
Prof. Carlos Alexandre Barros de Melo (UFPE / Centro de Informática
Prof. Alexandre Cabral Mota(UFPE / Centro e Informática)
Prof. Marcel Vinicius Medeiros Oliveira (UFRN/Depto. de Informática e Matemática Aplicada)
Prof. Adenilso da Silva Simão (USP / ICMC )
RESUMO:
Sistemas ciber-físicos (CPSs) integram sistemas computacionais em seus
ambientes físicos; componentes para produtos como automóveis e aviões são
exemplos de CPSs modernos. A complexidade de tais sistemas vem de seu
\emph{design} multidisciplinar que tipicamente compreende elementos
discretos e contínuos. A importância da segurança e confiabilidade destes
sistemas justifica a necessidade de mais pesquisas sobre sua verificação.
Neste trabalho, propõe-se um \textit{framework} formal para teste (de
conformidade) e análise (de causalidade) de sistemas ciber-físicos. O
\textit{framework} é dividido em duas etapas: i) uma abordagem de teste
baseada em uma busca multi-objetivos que gera entradas efetivas para
encontrar falhas em CPSs e ii) uma noção de causalidade que atribui causas
para os eventos que levaram a essas falhas.
Na busca multi-objetivos proposta, o principal intuito é fornecer sinais de
entrada para um sistema de forma a maximizar a distância entre a saída do
sistema e de um alvo ideal, levando o sistema a uma falha. Além disso,
leva-se em consideração os estados discretos (dos modelos de sistemas
híbridos) e uma noção de diversidade de entradas para aumentar a cobertura.
A estratégia proposta foi implementada e este trabalho apresenta também
análises empíricas para mostrar sua eficácia.
Quanto à análise de causalidade, o primeiro passo é formalizar uma noção de
falhas e causas usando notações matemáticas. As falhas são representadas
usando uma simplificação de proposições em lógica temporal de sinal (STL),
e as causas são expressas usando intervalos de trajetórias que levaram à
falsificação de tais propriedades. Para aplicar a causalidade em sistemas
contínuos, é preciso levar o tempo em consideração. Uma falha que ocorreu
em um determinado momento pode ter sido causada por eventos muito
anteriores. Dessa forma, o objetivo desse trabalho é identificar não apenas
a quais componentes a falha deve ser atribuída, mas também fornecer o
momento no tempo.
As contribuições deste trabalho podem ser resumidas da seguinte forma.
Propõe-se um \textit{framework} para testar e analisar CPSs. A abordagem de
teste utiliza uma estratégia de busca multi-objetivos para seleção de
entradas que maximizam a chance de identificar uma falha (i.e., uma
violação de conformidade). Leva-se em conta os contraexemplos produzidos e
aplica-se causalidade como uma ferramenta para interpretar tais testemunhas
da violação de conformidade. Para isso, estende-se uma teoria de
causalidade (originalmente para sistemas discretos) para lidar com os
aspectos contínuos de CPSs. Comparam-se os resultados com as abordagens
relacionadas, usando exemplos da literatura e estudos de caso que foram
desenvolvidos neste trabalho. A mecanização da estratégia é feita em
Matlab/Simulink, que é um ambiente comumente usado para modelagem e análise
de sistemas de controle, aumentando assim a acessibilidade à estratégia
proposta nesse trabalho.
Palavras-chave: sistemas ciber-físicos, teste de conformidade, testes
baseados em buscas, causalidade
Comentários desativados