A rigorous architectural approach to development component-based software systems

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 apresenta uma abordagem rigorosa e centrada na arquitetura para o desenvolvimento de sistemas de software tolerantes a falhas. Dependendo do modelo de falhas e da disponibilidade de recursos, abstrações arquiteturais 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 e métodos formais e casos de teste baseados em modelos para sistematizar a verificação e validação do comportamento do sistema relativo à programação e tratamento de erros e tratamento de falhas no nível arquitetural. A verificação e validação de software ocorrem em duas fases complementares do processo de desenvolvimento do software, ambas baseadas em cenários arquiteturais que descrevem a programação e tratamento de erros envolvendo elementos arquiteturais (componentes e conectores). Primeiramente, utilizando a ferramenta de verificação 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 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 existe 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 três estudos de caso: (i) uma aplicação com requisitos críticos de tempo real e confiabilidade; (ii) uma aplicação bancária real com requisitos críticos de confiabilidade e disponibilidades; e (iii) uma aplicação para dispositivos móveisThe incorporation of fault tolerance into systems normally increases their complexity, which consequently makes their analysis more difficult. Moreover, the use of exception handling mechanisms to develop robust software systems in a non-systematic manner can be a source of many design faults. This thesis presents a rigorous and architecture-centric development approach for developing fault-tolerant software systems. Depending on the fault model and the resources available, different architectural abstractions can be employed for representing issues that are related to fault tolerance, such as error detection, and error and fault handling. These architectural abstractions and their internal views can be instantiated into concrete components and connectors for designing fault-tolerant software architectures. In a complementary way, the proposed rigorous solution also defines activities which use formal methods and model-based test cases do systematize the verification and validation of the system's behaviour related to error propagation and handling at the architecture level. The verification and validation occur in two complementary phases of the software development, both of them based on architectural scenarios describing error propagation and handling involving architectural elements (components and connectors). First, using the ProB model checker, which combines the use of set-theory (B-Method) and process algebra (CSP), the software architecture is formally verified in order to anticipate the identification of faults related to the system's model. Second, model-based test cases are generated in order to assess the consistency between the verified software architecture and the implementation of the software system. Finally, the proposed solution also defines rules for model transformation from UML diagrams to formal specification in B-Method and CSP. To overcome the gap between the semi-formal specification of UML and the formal models, the UML diagrams are complemented with predefined stereotypes and tags. The feasibility of our approach was evaluated in the context of three case studies: (i) a critical real-time application; (ii) a real banking system; and (iii) a mobile applicatio