JFORTES: Java Formal Unit TESt Generation

The use of computer-based systems has increased significantly over the last years in several domains, mainly when we take into account the applications running on mobile platforms that have exploded in just a few short years, so that software verification and testing now play an important role in ensuring the overall product quality. In this paper, we describe the preliminary results of a work that presents a method to integrate formal verification techniques adopting ESC/Java2 and JCute tools with unit testing by TestNG framework to verify Java programs. This method aims to extract the safety properties generated by ESC/Java2 to automatically generate test cases using the rich set of assertions provided by the TestNG framework and JCute to validate those test cases. It is worth noting that is widely recognized that there is a growing need for automated testing techniques aimed at mobile applications, in platforms, such as: Android or Java Platform, Micro Edition (Java ME). Additionally, a critical challenge is the systematic generation of test cases. We show preliminary results of our proposed method over publicly available benchmarks, and compare the results to recognized tools, e.g., CBMC and JavaPathFinder. Experimental results show that our proposed method detects 86.04% of correct results (i.e., if a property satisfy its specification or is violated), while CBMC has found 79.06%, and JPF has found 93,02%.