Banca de QUALIFICAÇÃO: SAMUEL LINCOLN MAGALHAES BARROCAS

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : SAMUEL LINCOLN MAGALHAES BARROCAS
DATA : 14/02/2017
HORA: 09:00
LOCAL: IMD - CIVT B321
TÍTULO:

A Strategy to validate the Code Generator from Circus to Java


PALAVRAS-CHAVES:

Formal Methods, model-checking, validation, Circus.


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:
Formal Methods are techniques used to prevent errors on the development of Software Systems. As the process of developing Software from Formal methods is laborious and error-prone, Formal Code Generators are used. The use of these tools reduces error odds on the implementation of Software Systems from Formal Specifications. As there can be errors also on the process of generation of the Software from the input Specification, an interesting effort is to prove that the generated code correctly implements the input specification. This Qualifying Doctorate Proposal aims at elaborating a coverage and code-model-checking based strategy to validate JCircus, a translator from concrete Circus’ specifications to Java code. This validation strategy encompasses the implementation of a Labelled Transition System Generator (LPTSGen) for Circus (based on a Structural Operational Semantics for Circus ) and its conversion to JPF (Java Pathfinder), a Java model checker. The goal is to check if the specification is refined by the generated code by JCircus. In order to achieve this goal, the JPF model must conduct the generated code by JCircus. 
 
This Doctorate Proposal also shows partial results on the proof of soundness of the rules of the Structural Operational Semantics with respect to the Unifying Theories of Programming (UTP). The role of the proof of soundness is to strenghten the validation.

MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1709820 - ROBERTA DE SOUZA COELHO
Notícia cadastrada em: 09/02/2017 21:26
SIGAA | Superintendência de Informática - | | Copyright © 2006-2020 - UFRN - sigaa06-producao.info.ufrn.br.sigaa06-producao