A formally founded framework for dynamic software architectures - Cavalcante, Everton Ranielly de Sousa (2016)
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.