International Association of Engineers
While software testing concerns the efficient test case design and test procedure to unveil the software defects, it is difficult to conduct the testing of the complicated and concurrent software. The formal verification of the software source code is considered as the complementary to the conventional testing. The verification model is expected and it is possibly extracted from the source code using automated scheme. Several researches have already provided the appropriate high level guidelines to translate Java into formal verification model. In this paper, they propose a development of an automated translation tool of Java source code into Proemial. The Java control flows and basic arithmetic and logical operators are focused due to the specific data types and control flows in Promela.