Use este identificador para citar ou linkar para este item:
https://repositorio.ufpe.br/handle/123456789/52376
Compartilhe esta página
Registro completo de metadados
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.advisor | SAMPAIO, Augusto Cezar Alves | - |
dc.contributor.author | ARAUJO, Hugo Leonardo da Silva | - |
dc.date.accessioned | 2023-09-22T12:06:56Z | - |
dc.date.available | 2023-09-22T12:06:56Z | - |
dc.date.issued | 2023-03-23 | - |
dc.identifier.citation | ARAUJO, Hugo Leonardo da Silva. A framework for testing cyber-physical systems: input generation and causal analysis. 2023. Tese (Doutorado em Ciência da Computação) – Universidade Federal de Pernambuco, Recife, 2023. | pt_BR |
dc.identifier.uri | https://repositorio.ufpe.br/handle/123456789/52376 | - |
dc.description.abstract | Cyber-Physical Systems (CPSs) integrate computational systems into their physical environments; components for products such as automobiles and airplanes are examples of modern CPSs. Their complexity originates from their multidisciplinary design which typically comprises discrete and continuous elements. The importance of safety and relia- bility in such complex and heterogeneous systems warrants the need for further research into their verification. In this work, we propose a framework for (conformance) testing and (causality) analysis of cyber-physical systems. The framework is divided into two stages, i) a search-based testing approach that generates effective inputs for finding faults in CPSs and ii) a notion of causality that assigns causes for the events that led to such faults. In our multi-objective search strategy the main goal is to provide input signals for a system in such a way that they maximise the distance between the system’s output and its ideal one, thus leading the system towards a fault. Additionally, we take into consideration the discrete locations (of hybrid system models) and a notion of input di- versity to increase coverage. We implement our strategy and present empirical analyses to estimate its effectiveness. As for the causality analysis, we formalised a notion of faults and causes using mathematical notations. Although these notions have been previously formalised for discrete systems, there is no formal account for continuous systems. Since the inputs and outputs of our systems are represented by trajectories (i.e., signals) the faults are expressed using a simplification of signal temporal logic properties, and causes, using the slices of trajectories that led to the falsification of such properties. To apply causality to cyber-physical systems, one needs to take time into consideration. A fault that occurred at a particular point in time could have been caused by events that oc- curred much earlier. Thus, one cannot ignore the history of the system execution. This way, we aim to identify not only which component should the fault be attributed to but also provide the moment in time. The contributions of this work can be summarised as follows. We propose a framework to test and analyse CPSs. Our testing strategy makes use of a multi-objective search strategy for input selection that maximises the likelihood of identifying a fault (i.e., a conformance violation). We consider the counterexamples produced in the testing phase and employ causality as a reasoning tool to interpret these witnesses to conformance violation. For that, we extended the theory of actual causality for discrete systems to cope with continuous aspects of CPSs. We contrast our results against related approaches using examples from the literature and our own case studies. The mechanisation of the strategy is done on the Matlab/Simulink framework, which is a commonly used environment for modelling and analysis of control systems, thus increasing the accessibility to our strategy. | pt_BR |
dc.description.sponsorship | CNPq | pt_BR |
dc.language.iso | eng | pt_BR |
dc.publisher | Universidade Federal de Pernambuco | pt_BR |
dc.rights | embargoedAccess | pt_BR |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/3.0/br/ | * |
dc.subject | Engenharia de software | pt_BR |
dc.subject | Teste de conformidade | pt_BR |
dc.title | A framework for testing cyber-physical systems : input generation and causal analysis | pt_BR |
dc.type | doctoralThesis | pt_BR |
dc.contributor.advisor-co | CARVALHO, Gustavo Henrique Porto de | - |
dc.contributor.advisor-co | MOUSAVI, Mohammadreza | - |
dc.contributor.authorLattes | http://lattes.cnpq.br/4993643802908151 | pt_BR |
dc.publisher.initials | UFPE | pt_BR |
dc.publisher.country | Brasil | pt_BR |
dc.degree.level | doutorado | pt_BR |
dc.contributor.advisorLattes | http://lattes.cnpq.br/3977760354511853 | pt_BR |
dc.publisher.program | Programa de Pos Graduacao em Ciencia da Computacao | pt_BR |
dc.description.abstractx | 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 design multidisciplinar que tipi- camente compreende elementos discretos e contínuos. A importância da segurança e con- fiabilidade destes sistemas justifica a necessidade de mais pesquisas sobre sua verificação. Neste trabalho, propõe-se um framework formal para teste (de conformidade) e análise (de causalidade) de sistemas ciber-físicos. O 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 di- versidade 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 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). Levam-se em conta os contraexemplos produzidos e aplica-se causalidade como uma ferramenta para interpretar tais testemunhas da violação de con- formidade. 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. | pt_BR |
dc.contributor.advisor-coLattes | http://lattes.cnpq.br/9603136866152813 | pt_BR |
Aparece nas coleções: | Teses de Doutorado - Ciência da Computação |
Arquivos associados a este item:
Arquivo | Descrição | Tamanho | Formato | |
---|---|---|---|---|
TESE Hugo Leonardo da Silva Araujo.pdf Item embargado até 2025-09-22 | 5,68 MB | Adobe PDF | Visualizar/Abrir Item embargado |
Este arquivo é protegido por direitos autorais |
Este item está licenciada sob uma Licença Creative Commons