A formally founded framework for dynamic software architectures

Software architectures play a significant role in the development of software-intensive systems in order to allow satisfying both functional and non-functional requirements. In particular, dynamic software architectures have emerged to address characteristics of the contemporary systems that oper...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Cavalcante, Everton Ranielly de Sousa
Outros Autores: Batista, Thais Vasconcelos
Formato: doctoralThesis
Idioma:por
Publicado em: Brasil
Assuntos:
Arquiteturas de software
Linguagens de descrição arquitetural
Reconfiguração dinâmica
Verificação formal
Lógica temporal
Verificação estatística
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/23763
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-23763
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language por
topic Arquiteturas de software
Linguagens de descrição arquitetural
Reconfiguração dinâmica
Verificação formal
Lógica temporal
Verificação estatística
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle Arquiteturas de software
Linguagens de descrição arquitetural
Reconfiguração dinâmica
Verificação formal
Lógica temporal
Verificação estatística
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Cavalcante, Everton Ranielly de Sousa
A formally founded framework for dynamic software architectures
description Software architectures play a significant role in the development of software-intensive systems in order to allow satisfying both functional and non-functional requirements. In particular, dynamic software architectures have emerged to address characteristics of the contemporary systems that operate on dynamic environments and consequently subjected to changes at runtime. Architecture description languages (ADLs) are used to represent software architectures, producing models that can be used at design time and/or runtime. However, most existing ADLs have limitations in several facets: (i) they are focused on structural, topological aspects of the architecture; (ii) they do not provide an adequate support for representing behavioral aspects of the architecture; (iii) they do not allow describing advanced aspects regarding the dynamics of the architecture; (iv) they are limited with respect to the automated verification of architectural properties and constraints; and (v) they are disconnected from the implementation level, thus entailing inconsistencies between architecture and implementation. In order to tackle these problems, this thesis proposes formally founded framework for dynamic software architectures. Such a framework comprises: (i) π-ADL, a formal language for describing software architectures under both structural and behavioral viewpoints; (ii) the specification of programmed dynamic reconfiguration operations; (iii) the automated generation of source code from architecture descriptions; and (iv) an approach based on statistical model checking (SMC) to formally express and verify properties in dynamic software architectures. The main contributions brought by the proposed framework are fourfold. First, the π-ADL language was endowed with architectural-level primitives for describing programmed dynamic reconfigurations. Second, architecture descriptions in π- ADL are translated towards implementation source code in the Go programming language, thereby contributing to minimize architectural drifts. Third, a novel logic, called DynBLTL, is used to formally express properties in dynamic software architectures. Fourth, a toolchain relying on SMC was built to automate the verification of architectural properties while striving to reduce effort, computational resources, and time for performing such a task. In this work, two wireless sensor network-based systems are used to validate the framework elements.
author2 Batista, Thais Vasconcelos
author_facet Batista, Thais Vasconcelos
Cavalcante, Everton Ranielly de Sousa
format doctoralThesis
author Cavalcante, Everton Ranielly de Sousa
author_sort Cavalcante, Everton Ranielly de Sousa
title A formally founded framework for dynamic software architectures
title_short A formally founded framework for dynamic software architectures
title_full A formally founded framework for dynamic software architectures
title_fullStr A formally founded framework for dynamic software architectures
title_full_unstemmed A formally founded framework for dynamic software architectures
title_sort formally founded framework for dynamic software architectures
publisher Brasil
publishDate 2017
url https://repositorio.ufrn.br/jspui/handle/123456789/23763
work_keys_str_mv AT cavalcanteevertonraniellydesousa aformallyfoundedframeworkfordynamicsoftwarearchitectures
AT cavalcanteevertonraniellydesousa umframeworkformalparaarquiteturasdesoftwaredinamicas
AT cavalcanteevertonraniellydesousa formallyfoundedframeworkfordynamicsoftwarearchitectures
_version_ 1773961170465587200
spelling ri-123456789-237632017-11-05T02:10:54Z A formally founded framework for dynamic software architectures Um framework formal para arquiteturas de software dinâmicas Cavalcante, Everton Ranielly de Sousa Batista, Thais Vasconcelos http://lattes.cnpq.br/5065548216266121 http://lattes.cnpq.br/5521922960404236 Leite, Jair Cavalcanti http://lattes.cnpq.br/8133660776746187 Aquino Júnior, Gibeon Soares de Aquino http://lattes.cnpq.br/1254338144161360 Nakagawa, Elisa Yumi http://lattes.cnpq.br/7494142007764616 Cuesta, Carlos Enrique Drira, Khalil Cunha, Paulo Roberto Freire http://lattes.cnpq.br/2026295360734357 Oquendo, Flávio http://lattes.cnpq.br/4858001230775451 Arquiteturas de software Linguagens de descrição arquitetural Reconfiguração dinâmica Verificação formal Lógica temporal Verificação estatística CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO Software architectures play a significant role in the development of software-intensive systems in order to allow satisfying both functional and non-functional requirements. In particular, dynamic software architectures have emerged to address characteristics of the contemporary systems that operate on dynamic environments and consequently subjected to changes at runtime. Architecture description languages (ADLs) are used to represent software architectures, producing models that can be used at design time and/or runtime. However, most existing ADLs have limitations in several facets: (i) they are focused on structural, topological aspects of the architecture; (ii) they do not provide an adequate support for representing behavioral aspects of the architecture; (iii) they do not allow describing advanced aspects regarding the dynamics of the architecture; (iv) they are limited with respect to the automated verification of architectural properties and constraints; and (v) they are disconnected from the implementation level, thus entailing inconsistencies between architecture and implementation. In order to tackle these problems, this thesis proposes formally founded framework for dynamic software architectures. Such a framework comprises: (i) π-ADL, a formal language for describing software architectures under both structural and behavioral viewpoints; (ii) the specification of programmed dynamic reconfiguration operations; (iii) the automated generation of source code from architecture descriptions; and (iv) an approach based on statistical model checking (SMC) to formally express and verify properties in dynamic software architectures. The main contributions brought by the proposed framework are fourfold. First, the π-ADL language was endowed with architectural-level primitives for describing programmed dynamic reconfigurations. Second, architecture descriptions in π- ADL are translated towards implementation source code in the Go programming language, thereby contributing to minimize architectural drifts. Third, a novel logic, called DynBLTL, is used to formally express properties in dynamic software architectures. Fourth, a toolchain relying on SMC was built to automate the verification of architectural properties while striving to reduce effort, computational resources, and time for performing such a task. In this work, two wireless sensor network-based systems are used to validate the framework elements. Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) Arquiteturas de software exercem um papel significativo no desenvolvimento de sistemas intensivos de software a fim de permitir satisfazer tanto requisitos funcionais quanto nãofuncionais. Em particular, arquiteturas de software dinâmicas têm surgido para endereçar características dos sistemas contemporâneos que operam em ambientes dinâmicos e consequentemente sujeitos a mudanças em tempo de execução. Linguagens de descrição arquitetural (ADLs) são utilizadas para representar arquiteturas de software, produzindo modelos que podem ser utilizados tanto em tempo de projeto quanto em tempo de execução. Contudo, a maioria das ADLs existentes possui limitações em diversos aspectos: (i) possui enfoque em aspectos estruturais, topológicos da arquitetura; (ii) não provê um suporte adequado à representação de aspectos comportamentais da arquitetura; (iii) não permite descrever aspectos avançados relativos à dinâmica da arquitetura; (iv) é limitada com relação à verificação de propriedades arquiteturais e restrições, e; (v) é desconectada do nível de implementação, resultando em inconsistências entre arquitetura e implementação. No intuito de endereçar esses problemas, esta tese propõe um framework formal para arquiteturas de software dinâmicas. Tal framework envolve: (i) π-ADL, uma linguagem formal para descrever arquiteturas de software sob as perspectivas estrutural e comportamental; (ii) a especificação de operações de reconfiguração dinâmica programada; (iii) a geração automática de código fonte a partir de descrições arquiteturais, e; (iv) uma abordagem baseada em verificação estatística (SMC) para expressar e verificar formalmente propriedades em arquiteturas de software dinâmicas. As principais contribuições trazidas pelo framework proposto são quatro. Primeiro, a linguagem π-ADL passou a ser dotada de primitivas de nível arquitetural para descrever reconfigurações dinâmicas programadas. Segundo, descrições arquiteturais em π-ADL são traduzidas para código fonte de implementação na linguagem de programação Go, contribuindo assim para minimizar desvios arquiteturais. Terceiro, uma nova lógica chamada DynBLTL é utilizada para expressar formalmente propriedades em arquiteturas de software dinâmicas. Quarto, um ferramental baseado em SMC foi construído para automatizar verificação de propriedades arquiteturais enquanto busca reduzir esforço, recursos computacionais e tempo para realizar essa tarefa. Neste trabalho, dois sistemas baseados em redes de sensores sem fio são utilizados para validar os elementos do framework. 2017-08-14T11:42:00Z 2017-08-14T11:42:00Z 2016-06-10 doctoralThesis CAVALCANTE, Everton Ranielly de Sousa. A formally founded framework for dynamic software architectures. 2016. 168f. Tese (Doutorado em Ciência da Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2016. https://repositorio.ufrn.br/jspui/handle/123456789/23763 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO

Registros relacionados