Advanced search
Start date

Generation of Java pathfinder properties from test purposes

Grant number: 13/22317-6
Support type:Scholarships abroad - Research Internship - Doctorate
Effective date (Start): March 17, 2014
Effective date (End): January 17, 2015
Field of knowledge:Physical Sciences and Mathematics - Computer Science - Computing Methodologies and Techniques
Principal researcher:Ana Cristina Vieira de Melo
Grantee:Simone Hanazumi
Supervisor abroad: Corina Pasareanu
Home Institution: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brazil
Research place: Carnegie Mellon University (CMU), United States  
Associated to the scholarship:11/01928-1 - Generation of Java Programs Properties from Test Purposes, BP.DR


This Research Internship Abroad (BEPE) project is part of the Ph.D work under the São Paulo Research Foundation (FAPESP) process: 2011/01928-1. The main objective of the Ph.D work is to help software developers in applying formal verification in practice. To do this, we propose an approach that generates the corresponding source code of the system properties that should be verified to assure the software quality. This code generation will be guided by the test purposes derived from the system specification.The main challenge of the Ph.D research is to synchronize the test purposes at implementation and specification levels in order to automate the properties code generation. To solve this problem, we have decided to make a theoretical work over this synchronization and then apply its results in practice using the Java PathFinder (JPF), a virtual machine that can be used as a model checker to verify Java programs. In this BEPE project, we will focus on the application of the theoretical results in practice: we will proceed to the implementation of general properties templates in JPF. These templates will be used to automate the generation of properties code that a system must satisfy to guarantee its quality. And the generated property code will be registered in JPF so that it will be able to check whether the system satisfies this property or not. To validate the implementation of those JPF general properties templates, a set of tests for each property template must be created and executed. (AU)

News published in Agência FAPESP Newsletter about the scholarship:
Articles published in other media outlets (0 total):
More itemsLess items

Scientific publications
(References retrieved automatically from Web of Science and SciELO through information on FAPESP grants and their corresponding numbers as mentioned in the publications by the authors)
HANAZUMI, SIMONE; DE MELO, ANA C. V.. A Formal Approach to implement java exceptions in cooperative systems. JOURNAL OF SYSTEMS AND SOFTWARE, v. 131, p. 475-490, . (13/22317-6, 12/23767-2, 11/01928-1)

Please report errors in scientific publications list by writing to: