FAILURE MODE AND EFFECT ANALYSIS - FORMAL VERIFICATION THROUGH A FAILURE MODE PROPAGATION APPROACH

Abstract

Análise de modos de falha e seus efeitos (FMEA), é uma técnica usada para mitigar ou remover falhas de um serviço, produto ou processo, identificando seus modos de falha, causes, efeitos e possíveis medidas de mitigação. A documentação desta análise é feita com o preenchimento de uma grelha, onde cada linha representa um modo de falha e onde estão as descrições dos seus efeitos, causas e medidas de mitigação. Alguns dos principais problemas da técnica estão na dificuldade em representar de forma consistente as propagações de falha entre componentes, as causas, efeitos e medidas de mitigação dos modos de falha e na manutenção da grelha que documenta a FMEA. Esta dissertação formaliza a FMEA de modo a tornar possível por meio da verificação formal de sua documentação, que a análise foi feita corretamente e que os dados nela representados são consistência com as propriedades estabelecidas na verificação. Promela, uma linguagem que permite a especificação formal de sistemas, é usada para implementar a representação dos modos de falha, seus atributos, medidas de mitigação e propagações de falhas. O Spin model checker usa então as propriedades previamente estabelecidas para verificar se o sistema representado é seguro ou não, considerando todas as propagações de falhas e medidas de mitigação. Além do mais, um novo formato para a documentação da FMEA é proposto de modo a ser possível a extração do modelo Promela por meio da representação em grelha da FMEA usando para isso um tradutor. É esperado que com esta solução a FMEA ganhe consistência na forma como seus modos de falha, medidas de mitigação e propagações de falha são representados e que isso reduza o esforço na condução da análise. Apesar de ter conseguido adquirir maior consistência na análise, os casos testados onde não existiam ameaças para a segurança do sistema não tiveram verificações bem sucedidas, devido à explosão de estados comum no model checking, no entanto, a verificação foi bem sucedida ao identificar todos os casos onde haviam ameaças a segurança.

Failure Mode and Effects Analysis (FMEA) is the name given to a technique used to mitigate or remove failures from services, products and processes by the identification of failure modes, their causes, effects and possible mitigation measures. The documentation of this analysis is usually done by filling a spreadsheet where each row is a failure mode, and there are textual descriptions of the effects, causes and mitigation measures. Some of the main issues of FMEA are the consistent representation of failure propagations between components, maintenance of FMEA tables and use of the same designation of causes, effects and mitigation measures. This Dissertation formalise the FMEA documentation so as to use a model checking to verify the correctness and consistency of the analysis. Promela, a formal specification language, is used to implement a model that represents failure modes, it’s attributes, mitigation measures and propagation of failures. The Spin model checker is then able to verify the FMEA risk threshold considering all the failure propagations and mitigation measures. In addition, a new format for the FMEA table is proposed, so the information of a system/product/service architecture description from the spreadsheet is extracted to a Promela model using a simple translator implemented in Python. We expect that with this solution, FMEA will gain consistency on it’s representation of failure modes, mitigation measures and failure propagations and that it will reduce the effort required to verify failure propagation chains. Whereas the consistency on the FMEA data representation were achieved, the verification of the system was not capable of finishing a verification run in FMEA’s spreadsheets that contained no threats to the system’s safety due to the state explosion cause by the model checking, however, the verification was successful in identify the cases were threats to the safety of the system were present in the FMEA’s spreadsheet.