| dc.contributor | Batista, Thais Vasconcelos | |
| dc.contributor | https://orcid.org/0000-0003-3558-1450 | |
| dc.contributor | http://lattes.cnpq.br/5521922960404236 | |
| dc.contributor | Cavalcante, Everton Ranielly de Sousa | |
| dc.contributor | https://orcid.org/0000-0002-2475-5075 | |
| dc.contributor | http://lattes.cnpq.br/5065548216266121 | |
| dc.contributor | Oquendo, Flávio | |
| dc.contributor | Oliveira, Lucas Bueno Ruas de | |
| dc.contributor | Oliveira, Marcel Vinicius Medeiros | |
| dc.creator | Araújo, Camila de | |
| dc.date | 2023-07-13T21:00:37Z | |
| dc.date | 2023-07-13T21:00:37Z | |
| dc.date | 2023-03-31 | |
| dc.date.accessioned | 2023-09-04T12:07:30Z | |
| dc.date.available | 2023-09-04T12:07:30Z | |
| dc.identifier | 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. | |
| dc.identifier | https://repositorio.ufrn.br/handle/123456789/53351 | |
| dc.identifier.uri | https://repositorioslatinoamericanos.uchile.cl/handle/2250/8599185 | |
| dc.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. | |
| dc.description | 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. | |
| dc.format | application/pdf | |
| dc.language | pt_BR | |
| dc.publisher | Universidade Federal do Rio Grande do Norte | |
| dc.publisher | Brasil | |
| dc.publisher | UFRN | |
| dc.publisher | PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO | |
| dc.rights | Acesso Aberto | |
| dc.subject | Computação | |
| dc.subject | Software architecture | |
| dc.subject | Architectural description language | |
| dc.subject | Model-driven development | |
| dc.subject | Formal verification | |
| dc.subject | SysADL | |
| dc.subject | Pi-ADL | |
| dc.subject | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO | |
| dc.title | Enriching SysML-based software architecture descriptions: a model-driven approach | |
| dc.type | doctoralThesis | |
