Model-based Testing with Modbat for JPF

Modbat is a model-based testing framework that utilizes finite state machines (FSMs) to generate tests systematically, exploring various execution paths based on predefined models. Java PathFinder (JPF) is a powerful model checking tool that verifies Java programs by exhaustively exploring their state space.The primary objective of this project is to integrate Modbat with JPF to improve the effectiveness and efficiency of test generation for Java applications. By combining the model-based approach of Modbat with the exhaustive verification capabilities of JPF, we aim to achieve comprehensive test coverage while minimizing redundant test cases.