Enriching SysML-based software architecture descriptions: a model-driven approach

The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML,...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Araújo, Camila de
Outros Autores: Batista, Thais Vasconcelos
Formato: doctoralThesis
Idioma:pt_BR
Publicado em: Universidade Federal do Rio Grande do Norte
Assuntos:
Computação
Software architecture
Architectural description language
Model-driven development
Formal verification
SysADL
Pi-ADL
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:https://repositorio.ufrn.br/handle/123456789/53351
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-53351
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language pt_BR
topic Computação
Software architecture
Architectural description language
Model-driven development
Formal verification
SysADL
Pi-ADL
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle Computação
Software architecture
Architectural description language
Model-driven development
Formal verification
SysADL
Pi-ADL
CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Araújo, Camila de
Enriching SysML-based software architecture descriptions: a model-driven approach
description The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML, SysML, and their derivatives to describe the structure and behavior of software architectures. However, these semi-formal notations have limitations regarding the support for architectural analysis, particularly formal verification. This work investigates how to formally support SysML-based architecture descriptions to enable the formal verification of software architectures. As a result of this research, the main contribution is proposing a model-driven approach (MDD) that provides formal semantics to a SysML-based architectural language, SysADL, through a seamless transformation of SysADL architecture descriptions to the corresponding formal specifications in p-ADL, a well-founded theoretically language based on the higher-order typed p-calculus. The proposal implementation involves the execution of a four-phase process: (i) Model-to-Model (M2M) transformation of SysADL models into p-ADL model; (ii) Modelto-text (M2T) transformation of p-ADL models into p-ADL source; (iii) corresponding executable architecture generation, and architecture validation; and (iv) property verification. The work has other associated contributions to support the 4-phase process: (i) a denotational semantics to SysADL in p-ADL; (ii) a definition of a process to support the automated transformation of SysADL models into p-ADL models; (iii) The validation of the p-ADL architecture generated by the MDD transformation to demonstrate that it is in accordance with the original SysADL architecture; and (iv) the verification of formal architectural properties analyzing execution traces. The proposal was implemented and validated using a Flood Monitoring System architecture.
author2 Batista, Thais Vasconcelos
author_facet Batista, Thais Vasconcelos
Araújo, Camila de
format doctoralThesis
author Araújo, Camila de
author_sort Araújo, Camila de
title Enriching SysML-based software architecture descriptions: a model-driven approach
title_short Enriching SysML-based software architecture descriptions: a model-driven approach
title_full Enriching SysML-based software architecture descriptions: a model-driven approach
title_fullStr Enriching SysML-based software architecture descriptions: a model-driven approach
title_full_unstemmed Enriching SysML-based software architecture descriptions: a model-driven approach
title_sort enriching sysml-based software architecture descriptions: a model-driven approach
publisher Universidade Federal do Rio Grande do Norte
publishDate 2023
url https://repositorio.ufrn.br/handle/123456789/53351
work_keys_str_mv AT araujocamilade enrichingsysmlbasedsoftwarearchitecturedescriptionsamodeldrivenapproach
_version_ 1773957776673865728
spelling ri-123456789-533512023-07-13T21:01:07Z Enriching SysML-based software architecture descriptions: a model-driven approach Araújo, Camila de Batista, Thais Vasconcelos https://orcid.org/0000-0003-3558-1450 http://lattes.cnpq.br/5521922960404236 Cavalcante, Everton Ranielly de Sousa https://orcid.org/0000-0002-2475-5075 http://lattes.cnpq.br/5065548216266121 Oquendo, Flávio Oliveira, Lucas Bueno Ruas de Oliveira, Marcel Vinicius Medeiros Computação Software architecture Architectural description language Model-driven development Formal verification SysADL Pi-ADL CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO The critical nature of many complex software-intensive systems requires formal architecture descriptions for supporting automated architectural analysis regarding correctness properties. Due to the challenges of adopting formal approaches, many architects have preferred using notations such as UML, SysML, and their derivatives to describe the structure and behavior of software architectures. However, these semi-formal notations have limitations regarding the support for architectural analysis, particularly formal verification. This work investigates how to formally support SysML-based architecture descriptions to enable the formal verification of software architectures. As a result of this research, the main contribution is proposing a model-driven approach (MDD) that provides formal semantics to a SysML-based architectural language, SysADL, through a seamless transformation of SysADL architecture descriptions to the corresponding formal specifications in p-ADL, a well-founded theoretically language based on the higher-order typed p-calculus. The proposal implementation involves the execution of a four-phase process: (i) Model-to-Model (M2M) transformation of SysADL models into p-ADL model; (ii) Modelto-text (M2T) transformation of p-ADL models into p-ADL source; (iii) corresponding executable architecture generation, and architecture validation; and (iv) property verification. The work has other associated contributions to support the 4-phase process: (i) a denotational semantics to SysADL in p-ADL; (ii) a definition of a process to support the automated transformation of SysADL models into p-ADL models; (iii) The validation of the p-ADL architecture generated by the MDD transformation to demonstrate that it is in accordance with the original SysADL architecture; and (iv) the verification of formal architectural properties analyzing execution traces. The proposal was implemented and validated using a Flood Monitoring System architecture. A natureza crítica de muitos sistemas complexos de uso intensivo de software requer descrições formais de arquitetura para dar suporte à análise arquitetural automatizada em relação às propriedades de correção. Devido aos desafios de adotar abordagens formais, muitos arquitetos têm preferido usar notações como UML, SysML e seus derivados para descrever a estrutura e o comportamento das arquiteturas de software. No entanto, essas notações semi-formais têm limitações quanto ao suporte à análise arquitetural, principalmente à verificação formal. Este trabalho investiga como oferecer suporte formal a descrições de arquitetura baseadas em SysML para permitir a verificação formal de arquiteturas de software. Como resultado desta pesquisa, a principal contribuição é propor uma abordagem orientada a modelos (MDD) que fornece semântica formal para uma linguagem de arquitetura baseada em SysML, SysADL, por meio de uma transformação contínua das descrições da arquitetura SysADL para as especificações formais correspondentes em p-ADL, uma linguagem teoricamente bem fundamentada baseada no p-calculus de tipo de ordem superior. A implementação da proposta envolve a execução de um processo de 4 fases: (i) transformação modelo-a-modelo (M2M) de modelos SysADL em modelo p-ADL; (ii) transformação de modelo para texto (M2T) de modelos p-ADL em código p-ADL; (iii) geração de arquitetura executável correspondente e validação da arquitetura; e (iv) verificação de propriedades. O trabalho tem outras contribuições associadas para dar suporte ao processo de 4 fases: (i) uma semântica denotacional para SysADL; (ii) a definição de um processo para suportar a transformação automatizada de modelos SysADL em modelos p-ADL; (iii) A validação da arquitetura p-ADL gerada pela transformação MDD para mostrar que está de acordo com a arquitetura original SysADL; e (iv) a verificação de propriedades arquiteturais formais usando rastros de execução. A proposta foi implementada e validada utilizando uma arquitetura de Sistema de Monitoramento de Enchentes. 2023-07-13T21:00:37Z 2023-07-13T21:00:37Z 2023-03-31 doctoralThesis ARAÚJO, Camila de. Enriching SysML-based software architecture descriptions: a model-driven approach. Orientador: Thais Vasconcelos Batista. 2023. 174f. Tese (Doutorado em Ciência da Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2023. https://repositorio.ufrn.br/handle/123456789/53351 pt_BR Acesso Aberto application/pdf Universidade Federal do Rio Grande do Norte Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO

Registros relacionados