Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2015. / Submitted by Ana Cristina Barbosa da Silva (annabds@hotmail.com) on 2015-04-27T15:56:38Z No. of bitstreams: 1 2015_DaniloFilgueiraMendonça.pdf: 15442097 bytes, checksum: 3fd8f92515216f0962560e658342894f (MD5) / Approved for entry into archive by Raquel Viana(raquelviana@bce.unb.br) on 2015-05-14T19:16:39Z (GMT) No. of bitstreams: 1 2015_DaniloFilgueiraMendonça.pdf: 15442097 bytes, checksum: 3fd8f92515216f0962560e658342894f (MD5) / Made available in DSpace on 2015-05-14T19:16:39Z (GMT). No. of bitstreams: 1 2015_DaniloFilgueiraMendonça.pdf: 15442097 bytes, checksum: 3fd8f92515216f0962560e658342894f (MD5) / Um contexto de operação estático não é a realidade para muitos sistemas de software atualmente. Variações de contextos impõe novos desafios ao desenvolvimento de sistemas seguros, o que inclui a ativação de falhas apenas em contextos específicos de operação. A engenharia de requisitos orientada a objetivos (GORE) explicita o ‘por quê’ dos requisitos de um sistema, isto é, a intencionalidade por trás de objetivos do sistema e os meios de se atingi-los. Um Runtime goal model (RGM) adiciona especificação de comportamento ao modelo de objetivos convencional, enquanto um Contextual goal model (CGM) especifica efeitos de contextos sobre objetivos, meios e métricas de qualidade. Visando uma verificação formal da dependabilidade de um Contextual-Runtime goal model (CRGM), nesse trabalho é proposta uma nova abordagem para a análise de dependabilidade orientada a objetivos baseada na técnica de verificação probabilística de modelos. Em particular, são definidas regras para a transformação de um CRGM para um modelo cadeia de Makov de tempo discreto (DTMC) com o qual se possa verificar a confiabilidade de se satisfazer um ou mais objetivos do sistema. Adicionalmente, para diminuir o esforço de análise e aumentar a usabilidade de nossa proposta, um gerador automatizado de código CRGM para DTMC foi implementado e integrado com sucesso à ferramenta gráfica que dá suporte às fases de modelagem e análise de objetivos da metodologia TROPOS. A verificação contextual de dependabilidade resultante reflete os requisitos no CRGM, que podem representar: o projeto de um sistema, cuja verificação ocorreria em fase de projetos; ou um sistema em execução, cujo comportamento pode ser verificado em tempo de execução como parte de uma análise de auto-adaptação com foco em dependabilidade. / A static and stable operation environment is not a reality for many systems nowadays. Context variations impose many threats to systems safety, including the activation of context specific failures. Goal-oriented requirements engineering (GORE) brings forward the ‘why’ of system requirements, i.e., the intentionality behind system goals and the means to meet then. A runtime goal model adds a behaviour specification layer to a conventional design goal model, and a contextual goal model specifies the context effects over system goals, means and qualitative metrics. In order to formally verify the dependability of a CRGM, we propose a new goal-oriented dependability analysis based on the probabilistic model checking technique. In particular, we define rules for the transformation of a CRGM into a DTMC model that can be verified for the reliability of the fulfilment of one or more system goals. Also, to mitigate the analysis overhead and increase the usability of our proposal, we have successfully implemented and integrated a CRGM to DTMC code generator to the graphical tool that supports the goal modelling and analysis phases of the TROPOS development methodology. The resulting contextual dependability verification reflects the system requirements in a CRGM, which may represent: a system-to-be, whose verification would take place at design-time; or a running system, whose behaviour can be verified at runtime as part of a self-adaptation analysis targeting dependability.