期刊名称：IAENG International Journal of Computer Science
印刷版ISSN：1819-656X
电子版ISSN：1819-9224
出版年度：2021
卷号：48
期号：2
语种：English
出版社：IAENG - International Association of Engineers
摘要：This paper presents an analysis method of detecting the inconsistencies between a Java Bytecode program and its formal specification expressed at the Bytecode level, using the Bytecode Modeling Language (BML). The main objective of our work is not only to check the execution code of the called method of a Java object class from a valid input state but also to show how these inconsistencies can be extracted from the Control Flow Graph of the Method Under Test. We believe that Java Bytecode programs can contain bugs that the techniques used for objected-oriented software testing do not necessarily detect from their Java source programs. The proposed formal model shows how both the BML assertions and the Java Bytecode program can be translated into the same model of constraints, and how they can be used for detecting non-conformances of the method under test.
