Banca de DEFESA: SAMUEL LINCOLN MAGALHAES BARROCAS

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : SAMUEL LINCOLN MAGALHAES BARROCAS
DATA : 22/02/2018
HORA: 14:00
LOCAL: IMD/CIVT - B321
TÍTULO:

A Strategy to verify the code generation from Circus to Java


PALAVRAS-CHAVES:

Formal Methods, Model-Checking, Software Testing, Code Synthesis, 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:

The use of Automatic Code Generators for Formal Methods not only minimizes efforts on the implementation of Software Systems, as also reduces the chance of existing errors on the execution of such Systems. These tools, however, can themselves have faults on their source codes that causes errors on the generation of Software Systems, and thus verification of such tools is encouraged. This PhD thesis aims at creating and developing a strategy to verify JCircus, an automatic code generator from a large subset of Circus to Java. The interest in Circus comes from the fact that it allows the specification of concurrent and state-rich aspects of a System in a straightforward manner. The strategy of verification consists on the following steps: (1) extension of the existing operational semantics to Circus and proof that it is sound with respect to the existing denotational semantics of circus in the Unifying Theories of Programming (UTP), a framework that allows proof and unification of different theories; (2) development and implementation of a strategy that refinement-checks the generated code by JCircus, through a toolchain that encompasses a Labelled Predicate Transition System (LPTS) Generator for Circus and a Model Generator that inputs this LPTS and generates an Oracle that uses the Java Pathfinder code model-checker that refinement-checks the generated code by JCircus. Combined with coverage-based testing techniques, we envisage improving the reliability of the Code Generation from Circus to Java.


MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Interno - 1495704 - UMBERTO SOUZA DA COSTA
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 02/01/2018 20:03
SIGAA | Superintendência de Informática - | | Copyright © 2006-2020 - UFRN - sigaa05-producao.info.ufrn.br.sigaa05-producao