Banca de QUALIFICAÇÃO: CAMILA DE ARAUJO

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : CAMILA DE ARAUJO
DATA : 27/07/2021
HORA: 09:00
LOCAL: Google Meet
TÍTULO:

Habilitando Verificação Formal de Arquitetura de Software Dinâmica baseada em SysML: Uma Abordagem Dirigida por Modelos

PALAVRAS-CHAVES:

Arquitetura de Software, Verificação Formal, Linguagem de Descrição Arquitetural, Transformação de Modelos, Arquiteturas Dinâmicas.

PÁGINAS: 80
RESUMO:

A natureza crítica de muitos sistemas intensivos software complexos requer descrições de arquitetura formais para dar suporte à análise arquitetural automatizada em relação às propriedades relacionadas com correção. Devido aos desafios de adotar abordagens formais, muitos arquitetos preferem 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 semiformais têm limitações em relação ao suporte para a análise arquitetural, particularmente a verificação formal. Este trabalho investiga como conciliar suporte formal e descrições de arquitetura baseada em SysML, para permitir a verificação formal de arquiteturas de software dinâmicas. A principal contribuição é propor uma abordagem baseada em modelo que: (i) fornece semântica formal para uma linguagem de descrição de arquiteturas baseada em SysML, SysADL, transformando descrições de arquitetura SysADL em especificações expressas em pi-ADL, uma linguagem teoricamente bem fundamentada baseada em picalculus, e (ii) permite a verificação formal de propriedades para arquiteturas dinâmicas. Esses recursos são integrados a um ambiente que facilita a modelagem de arquiteturas SysML e sua verificação formal.

MEMBROS DA BANCA:
Presidente - 1213777 - THAIS VASCONCELOS BATISTA
Interno - 2316877 - EVERTON RANIELLY DE SOUSA CAVALCANTE
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Externo ao Programa - 1149392 - JAIR CAVALCANTI LEITE
Externo à Instituição - FLAVIO OQUENDO - UBS