An algebra of temporal faults

Submitted by Fernanda Rodrigues de Lima (fernanda.rlima@ufpe.br) on 2018-08-20T19:24:25Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO André Luis Didier.pdf: 2994400 bytes, checksum: 1f1900b560b2718e135b5c6a0bd6f0b8 (MD5) / Rejected by Alice Araujo (alice.caraujo@ufpe.br), reason: on 2018-08-20T22:58:29Z (GMT) / Submitted by Fernanda Rodrigues de Lima (fernanda.rlima@ufpe.br) on 2018-08-20T22:59:40Z
No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO André Luis Didier.pdf: 2994400 bytes, checksum: 1f1900b560b2718e135b5c6a0bd6f0b8 (MD5) / Approved for entry into archive by Alice Araujo (alice.caraujo@ufpe.br) on 2018-08-24T21:21:00Z (GMT) No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO André Luis Didier.pdf: 2994400 bytes, checksum: 1f1900b560b2718e135b5c6a0bd6f0b8 (MD5) / Made available in DSpace on 2018-08-24T21:21:00Z (GMT). No. of bitstreams: 2
license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5)
DISSERTAÇÃO André Luis Didier.pdf: 2994400 bytes, checksum: 1f1900b560b2718e135b5c6a0bd6f0b8 (MD5)
Previous issue date: 2017-03-08 / Fault modelling is essential to anticipate failures in critical systems. Traditionally, Static Fault Trees are employed to this end, but Temporal and Dynamic Fault Trees have gained evidence due to their enriched power to model and detect intricate propagation of faults that lead to a failure. In a previous work, we showed a strategy based on the process algebra CSP and Simulink models to obtain fault traces that lead to a failure. From the fault traces we discarded the ordering information to obtain structure expressions for Static Fault Trees. Instead of discarding such an ordering information, it could be used to obtain structure expressions of Temporal or Dynamic Fault Trees. In this work we present: (i) an algebra of temporal faults (with a notion of fault propagation) to analyse systems’ failures, and prove that it is indeed a Boolean algebra, and (ii) a parametrized activation logic to express nominal and erroneous behaviours, including fault modelling, provided an algebra and a set of operational modes. The algebra allows us to inherit Boolean algebra’s properties, laws and existing reduction techniques, which are very beneficial for fault modelling and analysis. With expressions in the algebra of temporal faults we allow the verification of safety properties based on Static, Temporal or Dynamic Fault Trees. The logic created in this work can be combined with other algebras beyond those shown here. Being used with the algebra of temporal faults it is intended to help analysts to consider all possible situations in complex expressions with order-related operators, avoiding missing subtle (but relevant) faults combinations. Furthermore, our algebra of temporal faults tackles the NOT operator which has been left out in other works. We illustrate our work on simple but real case studies, some supplied by our industrial partner EMBRAER. Isabelle/HOL was used to mechanize the theorems proofs of the algebra of temporal faults. / A modelagem de falhas é essencial na antecipação de defeitos em sistemas críticos. Tradicionalmente, Árvores de Falhas Estáticas são empregadas para este fim, mas Árvores de Falhas Temporais e Dinâmicas têm ganhado evidência devido ao seu maior poder para modelar e detectar propagações complexas de falhas que levam a um defeito. Em um trabalho anterior, mostramos uma estratégia baseada na álgebra de processos CSP e modelos Simulink para obter rastros (sequências) de falhas que levam a um defeito. A partir dos rastros de falhas nós descartamos a informação de ordenamento para obter expressões de estrutura para Ávores de Falhas Estáticas. Ao contrário de descartar tal informação de ordenamento, poderíamos usá-la para obter expressões de estrutura para Árvores de Falhas Temporais ou Dinâmicas. No presente trabalho apresentamos: (i) uma álgebra temporal de falhas (com noção de propagação de falhas) para analisar defeitos em sistemas e provamos que ela é de fato uma álgebra Booleana, e (ii) uma lógica de ativação parametrizada para expressar comportamentos nominais e de falha, incluindo a modelagem de falhas a partir de uma álgebra e um conjunto de modos de operação. A álgebra permite herdar as propriedades de álgebras Booleanas, leis e técnicas de redução existentes, as quais são muito benéficas para a modelagem e análise de falhas. Com expressões na álgebra temporal de falhas nós permitimos a verificação de propriedades de segurança (safety) baseadas em Árvores de Falhas Estáticas, Temporais ou Dinâmicas. A lógica criada neste trabalho pode ser usada com outras álgebras além das apresentadas. Sendo usada em conjunto com a álgebra temporal de falhas, tem a intenção de ajudar os analistas a considerar todas as possíveis situações em expressões complexas com operadores relacionados ao ordenamento das falhas, evitando esquecer combinações de falhas sutis (porém relevantes). Além disso, nossa álgebra temporal de falhas trata operadores NOT, que têm sido deixados de fora em outros trabalhos. Nós ilustramos nosso trabalho com alguns estudos de caso simples, mas reais, fornecidos pelo nosso parceiro industrial, a EMBRAER. Isabelle/HOL foi utilizado para a mecanização das provas dos teoremas da álgebra temporal de falhas.

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/25855
Date08 March 2017
CreatorsDIDIER, André Luís Ribeiro
Contributorshttp://lattes.cnpq.br/2794026545404598, MOTA, Alexandre Cabral
PublisherUniversidade Federal de Pernambuco, Programa de Pos Graduacao em Ciencia da Computacao, UFPE, Brasil
Source SetsIBICT Brazilian ETDs
LanguageEnglish
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis
Sourcereponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE
RightsAttribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess

Page generated in 0.0019 seconds