Detalhes bibliográficos
Ano de defesa: |
2023 |
Autor(a) principal: |
ARAUJO, Hugo Leonardo da Silva |
Orientador(a): |
SAMPAIO, Augusto Cezar Alves |
Banca de defesa: |
Não Informado pela instituição |
Tipo de documento: |
Tese
|
Tipo de acesso: |
Acesso embargado |
Idioma: |
eng |
Instituição de defesa: |
Universidade Federal de Pernambuco
|
Programa de Pós-Graduação: |
Programa de Pos Graduacao em Ciencia da Computacao
|
Departamento: |
Não Informado pela instituição
|
País: |
Brasil
|
Palavras-chave em Português: |
|
Link de acesso: |
https://repositorio.ufpe.br/handle/123456789/52376
|
Resumo: |
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. |