Banca de DEFESA: CAMILA DE ARAUJO

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
STUDENT : CAMILA DE ARAUJO
DATE: 31/03/2023
TIME: 08:30
LOCAL: Google Meet
TITLE:

Enriching SysML-Based Software Architecture Descriptions: A Model-Driven Approach


KEY WORDS:

Software architecture, Architectural description language, Model-driven development, Formal verification,  SysADL.


PAGES: 95
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
SPECIALTY: Engenharia de Software
SUMMARY:

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 \piadl, a well-founded theoretically language based on the higher-order typed Pi-calculus. The proposal implementation involves the execution of a 4-phase process: (i) Model-to-Model (M2M) transformation of SysADL models into piadl model; (ii) Model-to-text (M2T) transformation of PI-ADL models into PI-ADL code; (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 as a function of PI-ADL; (ii) a definition of a process to support the automated transformation of SysADL models into piadl models; (iii) The validation of the PI-ADL architecture generated by the MDD transformation to show that it is in accordance with the original SysADL architecture; and (iv) the verification of formal architectural properties using execution traces. The proposal was implemented and validated using a Flood Monitoring System architecture.


COMMITTEE MEMBERS:
Presidente - 1213777 - THAIS VASCONCELOS BATISTA
Interno - 2316877 - EVERTON RANIELLY DE SOUSA CAVALCANTE
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Externo à Instituição - FLAVIO OQUENDO - UBS
Externo à Instituição - LUCAS BUENO RUAS DE OLIVEIRA
Notícia cadastrada em: 27/02/2023 21:46
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa10-producao.info.ufrn.br.sigaa10-producao