Banca de DEFESA: HUGO LEONARDO DA SILVA ARAUJO

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE: HUGO LEONARDO DA SILVA ARAUJO
DATA : 23/03/2023
HORA: 14:00
LOCAL: Virtual
TÍTULO:

A framework for testing cyber-physical systems: input generation 
and causal analysis

PALAVRAS-CHAVES:

sistemas ciber-físicos, teste de conformidade, testes 
baseados em buscas, causalidade

PÁGINAS: 215
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.

MEMBROS DA BANCA:
Externo à Instituição - ADENILSO DA SILVA SIMÃO - USP
Interno - 2331188 - ALEXANDRE CABRAL MOTA
Interno - 1736873 - CARLOS ALEXANDRE BARROS DE MELLO
Externo à Instituição - MARCEL VINICIUS MEDEIROS OLIVEIRA - UFRN
Presidente - 2228250 - NELSON SOUTO ROSA