Banca de QUALIFICAÇÃO: LUCIANO ALEXANDRE DE FARIAS SILVA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
STUDENT : LUCIANO ALEXANDRE DE FARIAS SILVA
DATE: 08/07/2021
TIME: 15:00
LOCAL: Remoto (Google Meet)
TITLE:

AUTOMATED GENERATION OF VERIFIED COMPETITIVE HARDWARE

KEY WORDS:

Formal Methods. CSP. VHDL. Code Generation.

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:

The complexity of development and analysis is inherent to systems in general, specially to concurrent systems. When we work with critical systems this becomes much more evident, as an inconsistency is usually associated with a high cost. The sooner we identify an inconsistency in the design of a system and remove it, the lower the cost. For this reason, it is common to use the most varied strategies to reduce the difficulty and problems faced in this process. One of these strategies is the use of formal methods, which can use process algebra for specification and analysis of competing systems, improving the understanding of the project and enabling the identification of possible inconsistencies even in the initial stages of the project, ensuring the accuracy and correctness of the system specified.

This work presents a proposal for translating the CSP process algebra operators into the hardware description language VHDL. CSP is a language that allows us to make a formal description of a concurrent system. VHDL is a hardware description language that can be compiled on an FPGA card.

Our translation proposal is exemplified by a case study of an intelligent elevator control system. We present its formal specification in CSP and then its translation into a VHDL code, which we synthesize on an FPGA board.

BANKING MEMBERS:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interna - 1882699 - MONICA MAGALHAES PEREIRA