Generation of Java Programs Properties from Test Purposes

• Grant number: 11/01928-1
• Support Opportunities: Scholarships in Brazil - Doctorate
• Start date: July 01, 2011
• End date: July 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
• Host Institution: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brazil
• Associated scholarship(s): 13/22317-6 - Generation of Java pathfinder properties from test purposes, BE.EP.DR

Abstract

The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people's lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses.One of the techniques used to this purpose is called programs formal verification. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties should be implemented in a verifier, which is the tool responsible for running the verification and for notifying which properties were satisfied or not. When the verification process finishes, the verifier will indicate to software developers the possible location of each code fault in the system.The disadvantages of using formal verification are the high cost to apply this technique in real systems, and the necessity of having people with experience in formal languages and formal methods. In addition, the implementation of properties related to a particular system in a verifier is a complex task.To help software developers in the application of formal verification in Java programs, this work proposes the generation of properties code, for direct use in a verifier, from test purposes derived from system formal requirements.

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, SEP 2017. (13/22317-6, 12/23767-2, 11/01928-1)

Academic Publications

(References retrieved automatically from State of São Paulo Research Institutions)

HANAZUMI, Simone. Generation of Java program properties from test purposes. 2015. Doctoral Thesis - Universidade de São Paulo (USP). Instituto de Matemática e Estatística (IME/SBI) São Paulo.