Generation of Java program properties from test purposes

Author(s)

Simone Hanazumi

• Document type: Doctoral Thesis
• Press: São Paulo.
• Institution: Universidade de São Paulo (USP). Instituto de Matemática e Estatística (IME/SBI)
• Defense date: 2015-10-29

Examining board members

Ana Cristina Vieira de Melo; Patricia Duarte de Lima Machado; Ricardo Luis de Azevedo da Rocha; Valdivino Alexandre Santiago Junior; Flavio Soares Correa da Silva

• Advisor: Ana Cristina Vieira de Melo

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 formal verification of programs. 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 are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict. (AU)

• FAPESP's process: 11/01928-1 - Generation of Java Programs Properties from Test Purposes
• Grantee: Simone Hanazumi
• Support Opportunities: Scholarships in Brazil - Doctorate