A incorporação de tolerância a falhas em sistemas de software normalmente acarreta em um aumento da complexidade, o que consequentemente torna a sua análise mais difícil. Além disso, o uso de mecanismos de tratamento de exceções de uma maneira não-sistemática pode acarretar na adição de novas falhas ao sistema.

Esta tese de doutorado apresenta uma abordagem rigorosa baseada em abstrações arquiteturais para o desenvolvimento de sistemas de software tolerantes a falhas. Dependendo do modelo de falhas e da disponibilidade de recursos, abstrações diferentes podem ser utilizadas para representar explicitamente questões relacionadas a tolerância a falhas, tais como  detecção e tratamento de erros e tratamento de falhas. Essas abstrações arquiteturais e os seus respectivos detalhamentos internos podem ser instanciados em componentes e conectores concretos durante o projeto de arquiteturas de software tolerantes a falhas. De forma complementar, a solução proposta também define atividades que combinam o uso de métodos formais e casos de teste baseados em modelos para sistematizar a verificação do comportamento do sistema relativo à propagação e tratamento de erros e tratamento de falhas no nível arquitetural.

A verificação proposta ocorre em duas fases complementares do processo de desenvolvimento do software, ambas baseadas em cenários arquiteturais que descrevem a propagação e tratamento de erros envolvendo elementos arquiteturais (componentes e conectores). Primeiramente, utilizando a ferramenta de checagem de modelos ProB, que combina o uso de teoria de conjuntos matemáticos  (B-Method) com álgebra de processos (CSP), a arquitetura de software é verificada formalmente com o intuito de antecipar a identificação de falhas relacionadas ao projeto do sistema. Segundo, casos de teste são gerados a partir da da arquitetura de software utilizando uma abordagem baseada em modelos. O objetivo dos casos de teste gerados é verificar a consistência entre os modelos arquiteturais já verificados formalmente e a implementação do sistema.

Finalmente, para auxiliar as atividades de verificação, a solução proposta também contempla a definição de regras de transformação automática de diagramas UML para especificação formal em B-Method e CSP. A diferença semântica existente entre a especificação semi-formal da UML e a especificação formal em B-Method e CSP é compensada utilizando-se estereótipos e "tags" nos modelos UML.

A aplicabilidade prática da solução proposta foi avaliada no contexto de dois estudos de caso: (i) uma aplicação com requisitos críticos de tempo real e confiabilidade; e (ii) uma aplicação bancária real com requisitos críticos de confiabilidade e disponibilidade.