Banca de QUALIFICAÇÃO: FAGNER MORAIS DIAS

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
STUDENT : FAGNER MORAIS DIAS
DATE: 13/10/2021
TIME: 14:00
LOCAL: Remoto (Google Meet)
TITLE:

FormAr: Software Architecture Formalization for Critical Smart Cities Applications

KEY WORDS:

Software architecture description, Formal verification, CSP, SysADL

PAGES: 100
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:

Errors during the software development may give rise to flaws in the system that can cause important damages. One of the most important stages in the software development process is modelling the system architecture, possibly using software architecture description languages~(ADLs). The ADLs currently adopted by industry for software-intensive systems are mostly semi-formal and essentially based on SysML and specialized profiles. These ADLs allow describing the structure and the behavior of the system. Besides, it is possible to generate executable models or generate code in a target programming language and simulate its behaviour. This, however, does not constitute proof that the system is correct or safe. This work proposes a novel approach for empowering SysML-based ADLs with formal verification supported by model checking. It presents a CSP-based semantics to SysADL models. Furthermore, this work presents how correctness properties can be formally specified using CSP, and how the FDR4 refinement model-checker can verify these correctness properties. Finally, we present the new extension to SysADL studio that allows the automated transformation from SysADL architecture descriptions to CSP processes and the verification of important system correctness properties. The whole approach is illustrated via a case study, which is also part of this document. This case study demonstrates the usefulness of our approach in practice.

BANKING MEMBERS:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interna - 1213777 - THAIS VASCONCELOS BATISTA