| Grant number: | 13/22317-6 |
| Support Opportunities: | Scholarships abroad - Research Internship - Doctorate |
| Start date: | March 17, 2014 |
| End date: | January 17, 2015 |
| Field of knowledge: | Physical Sciences and Mathematics - Computer Science - Computing Methodologies and Techniques |
| Principal Investigator: | Ana Cristina Vieira de Melo |
| Grantee: | Simone Hanazumi |
| Supervisor: | Corina Pasareanu |
| Host Institution: | Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brazil |
| Institution abroad: | Carnegie Mellon University (CMU), United States |
| Associated to the scholarship: | 11/01928-1 - Generation of Java Programs Properties from Test Purposes, BP.DR |
Abstract 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: | |
| More itemsLess items | |
| TITULO | |
| Articles published in other media outlets ( ): | |
| More itemsLess items | |
| VEICULO: TITULO (DATA) | |
| VEICULO: TITULO (DATA) | |