COMBAT is a toolset for verification and analysis of behavior of software components that are implemented in Java. It supports the SOFA and Fractal component models, and assumes that the formalism of behavior protocols is used for specification of component behavior.

As an input, the toolset accepts a XML file with definition of a component architecture (XML Schema) and a properties file with the configuration (example). Verification of Java implementation is performed for each primitive component in the given architecture.

The toolset uses Java PathFinder (JPF) as a core model checker and addresses the following issues related to verification of component Java code with JPF: no support for high-level properties (like obeying of a behavior specification), problem of missing environment, and state explosion.

More specifically, the toolset supports the following techniques:

External dependencies