A semi-formal approach for Java programs verification

Software testing approaches are the most used techniques for programs verification because they are simple and fast. However, because of their lack of exhaustiveness, they cannot be considered as an alternative to formal verification approaches. On the other hand, these ones ensure total correction but with an important cost. In addition, they cannot operate well if the verified model is not consistent with the implementation. This paper proposes a new verification approach that combines tests and formal verification. The new approach, called SEmi-FORmal verification of Java programs or simply SE4J, uses tests to build a formal probabilistic model. This one will be formally verified in order to detect possible design errors in the program. The proposed approach permits also to compare two programs and validate test cases. The paper presents some obtained results over a case study and explains possible uses of the proposed approach.