Made available in DSpace on 2014-06-12T15:59:55Z (GMT). No. of bitstreams: 2
arquivo5803_1.pdf: 2496332 bytes, checksum: b4666e127bf620dbcb7437f9d83c2344 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2010 / Faculdade de Amparo à Ciência e Tecnologia do Estado de Pernambuco / A análise da segurança (Safety Assessment) é um processo bem conhecido que serve para
garantir que as restrições de segurança de um sistema crítico sejam cumpridas. Dentro dele, a
análise de segurança quantitativa lida com essas restrições em um contexto numérico
(probabilístico).
Os métodos de análise de segurança, como a tradicional Fault Tree Analysis (FTA), são
utilizados no processo de avaliação da segurança quantitativo, seguindo as diretrizes de
certificação (por exemplo, a ARP4761 Guia de Práticas Recomendadas da Aviação). No
entanto, este método é geralmente custoso e requer muito tempo e esforço para validar um
sistema como um todo, uma vez que para uma aeronave chegam a ser construídas, em média,
10.000 árvores de falha e também porque dependem fortemente das habilidades humanas para
lidar com suas limitações temporais que restringem o âmbito e o nível de detalhe que a análise e
os resultados podem alcançar. Por outro lado, as autoridades certificadoras também permitem a
utilização da análise de Markov, que, embora seus modelos sejam mais poderosos que as
árvores de falha, a indústria raramente adota esta análise porque seus modelos são mais
complexos e difíceis de lidar. Diante disto, FTA tem sido amplamente utilizada neste processo,
principalmente porque é conceitualmente mais simples e fácil de entender.
À medida que a complexidade e o time-to-market dos sistemas aumentam, o interesse em
abordar as questões de segurança durante as fases iniciais do projeto, ao invés de nas fases
intermediárias/finais, tornou comum a adoção de projetos, ferramentas e técnicas baseados em
modelos. Simulink é o exemplo padrão atualmente utilizado na indústria aeronáutica.
Entretanto, mesmo neste cenário, as soluções atuais seguem o que os engenheiros já utilizavam
anteriormente. Por outro lado, métodos formais que são linguagens, ferramentas e métodos
baseados em lógica e matemática discreta e não seguem as abordagens da engenharia
tradicional, podem proporcionar soluções inovadoras de baixo custo para engenheiros.
Esta dissertação define uma estratégia para a avaliação quantitativa de segurança baseada na
análise de Markov. Porém, em vez de lidar com modelos de Markov diretamente, usamos a
linguagem formal Prism (uma especificação em Prism é semanticamente interpretada como um
modelo de Markov). Além disto, esta especificação em Prism é extraída de forma sistemática a
partir de um modelo de alto nível (diagramas Simulink anotados com lógicas de falha do
sistema), através da aplicação de regras de tradução. A verificação sob o aspecto quantitativo
dos requisitos de segurança do sistema é realizada utilizando o verificador de modelos de Prism,
no qual os requisitos de segurança tornam-se fórmulas probabilísticas em lógica temporal.
O objetivo imediato do nosso trabalho é evitar o esforço de se criar várias árvores de falhas
até ser constatado que um requisito de segurança foi violado. Prism não constrói árvores de
falha para chegar neste resultado. Ele simplesmente verifica de uma só vez se um requisito de
segurança é satisfeito ou não no modelo inteiro.
Finalmente, nossa estratégia é ilustrada com um sistema simples (um projeto-piloto), mas
representativo, projetado pela Embraer
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2651 |
| Date | 31 January 2010 |
| Creators | GOMES, Adriano José Oliveira |
| Contributors | MOTA, Alexandre Cabral |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0022 seconds