Banca de QUALIFICAÇÃO: CAMILA DE ARAUJO
Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.STUDENT : CAMILA DE ARAUJO
DATE: 27/07/2021
TIME: 09:00
LOCAL: Google Meet
TITLE:
Enabling Formal Verification of SysML-Based Dynamic Software Architecture: A Model-Driven Approach
KEY WORDS:
Software Architecture, Formal Verification, Architecture Description Language, Model Transformation, Dynamic Architectures.
PAGES: 80
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 sought support for architectural analysis, particularly formal verification. This work investigates how to conciliate formal support and SysML-based architecture descriptions, to enable the formal verification of dynamic software architectures. The main contribution is proposing a model-driven approach that: (i) provides formal semantics to a SysML-based architectural language, SysADL, by transforming SysADL architecture descriptions in specifications expressed in pi-ADL, a well-founded theoretically language based on the higher-order typed pi-calculus, and (ii) enables the formal verification of properties for dynamic architectures. These facilities are integrated into an environment that facilitates modeling SysML architectures and formally verifying them.
BANKING MEMBERS:
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