Banca de QUALIFICAÇÃO: DALAY ISRAEL DE ALMEIDA PEREIRA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : DALAY ISRAEL DE ALMEIDA PEREIRA
DATA : 10/02/2017
HORA: 09:00
LOCAL: Instituto Metrópole Digital - CIVT - Sala B321
TÍTULO:

An Extension of a Tool for Formal Support to Component-based Development

PALAVRAS-CHAVES:

Component-Based Systems, CSP, Automation, SMT, Deadlock

PÁGINAS: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

The component-based development of systems is considered an important evolution in the software development process. Using this approach, the system maintenance is facilitated, bringing more reliability and reuse. The composition of components (and their interactions), however, is still the main source of problems and requires a detailed analysis. Formal Methods are an accurate tool for system specification that has strong mathematical background which bring, among benefits, more safety. The formal method CSP allows the specification of concurrent systems and the verification of properties inherent to such systems. CSP has a set of tools for its verification, like FDR2 and FDR3. However, the verifications of some properties can take too much time, like, for intance, deadlock freedom verification. BRICK has emerged as a CSP based approach for developing asynchronous component-based systems, which guarantees deadlock freedom by construction. This approach uses CSP to specify the constraints and interactions between the components to allow a formal verification of the system. However, the pratical use of this approach can be too complex and cumbersome. In order to automate the use of the BRICK approach we have developed a tool (BTS - BRICK Tool Support) that automates the verification of component composition by automatically generating and checking the side conditions imposed by the approach using FDR2. But, due to the number and complexity of the verifications made in FDR2, the tool can take too much time in this process. In this work, we present an extension to BTS that improves the way how it make verifications by replacing FDR2 by FDR3 and adding a a SMT prover, that concurrently checks some properties of the specification. We also improved the case studies in order to evaluate our tool.

MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN