Overview
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:
- checking of Java code against the high-level property of obeying a behavior specification defined in behavior protocols
- automated generation of environment for isolated components (via EnvGen for JPF)
- construction of three models of component environment's behavior (inverted frame protocol, context protocol and calling & trigger protocol)
- detection of potential concurrency errors in Java code via static analysis (search for suspicious patterns)
- measurement of the degree of concurrency-related interaction among Java methods via the SVA metric
External dependencies
- Support for original behavior protocols (
orig-bp.jar) - Java PathFinder (
jpf.jar,env_jpf.jar,env_jvm.jar), http://babelfish.arc.nasa.gov/trac/jpf - Fractal (
fractal.jar), http://fractal.objectweb.org - SOFA 2 (
sofa2.jar), http://sofa.objectweb.org - JSAP (
JSAP-2.0.jar), http://www.martiansoftware.com/jsap - BCEL (
bcel.jar), http://jakarta.apache.org/bcel/ - ASM (
asm-all-2.2.3.jar), http://asm.objectweb.org - Commons Collections (
commons-collections-3.2.jar), http://commons.apache.org/collections/
Contributors
- Pavel Parízek <parizek@d3s.mff.cuni.cz>