COMBAT

Download

External dependecies

Publications

Component Behavior Analysis Toolset

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

Additional information about the techniques can be found in the related publications.

The toolset is maintained and supported by Pavel Parizek.

Download

  • Binary: zip
  • Source code: zip

External dependencies

Publications

2008 (2)

Refereed (journals/proceedings)

PDF, Link Parízek P., Plášil F.: Modeling of Component Environment in Presence of Callbacks and Autonomous Activities,
In Proceedings of TOOLS EUROPE 2008, Springer-Verlag, LNBIP, vol. 11, ISBN 3-540-69823-4, ISSN 1865-1348, pp. 2-21, June 2008

Ph.D. Theses

PDF Parízek P.: Formal Verification of Components in Java,
Ph.D. thesis, advisor: Frantisek Plasil, September 2008

2007 (5)

Refereed (journals/proceedings)

PDF, Link Parízek P., Plášil F., Kofroň J.: Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker,
In Proceedings of 30th IEEE/NASA Software Engineering Workshop (SEW-30), IEEE Computer Society, ISBN 0-7695-2624-1, ISSN 1550-6215, pp. 133-141, January 2007
PDF, Link Parízek P., Plášil F.: Partial Verification of Software Components: Heuristics for Environment Construction,
In Proceedings of 33rd EUROMICRO SEAA conference, IEEE Computer Society, ISBN 0-7695-2977-1, ISSN 1089-6503, pp. 75-82, August 2007
PDF, Link Parízek P., Plášil F.: Specification and Generation of Environment for Model Checking of Software Components,
In Proceedings of International Workshop on Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2006), ENTCS, Vol. 176, Issue 2, ISSN 1571-0661, pp. 143-154, May 2007
PDF, Link Parízek P., Plášil F.: Modeling Environment for Component Model Checking from Hierarchical Architecture,
In Proceedings of Formal Aspects of Component Software (FACS'06), ENTCS, Vol. 182, ISSN 1571-0661, pp. 139-153, June 2007

Technical Reports

PDF Parízek P., Plášil F.: Heuristic Reduction of Parallelism in Component Environment,
Tech. Report No. 2007/2, Dep. of SW Engineering, Charles University in Prague, March 2007

2006 (2)

Technical Reports

PDF Parízek P., Plášil F., Kofroň J.: Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker,
Tech. Report No. 2006/2, Dep. of SW Engineering, Charles University, January 2006
PDF Parízek P., Plášil F.: Modeling Environment for Component Model Checking from Hierarchical Architecture,
Published in Preliminary Proceedings of 3rd International Workshop on Formal Aspects of Component Software (FACS'06), Prague, Czech Republic, September 20-22, 2006, UNU-IIST Report No. 344, September 2006

2005 (1)

Technical Reports

PDF Parízek P., Plášil F.: Specification and Generation of Environment for Model Checking of Software Components,
Tech. Report No. 2005/5, Dep. of SW Engineering, Charles University, November 2005
Modified on 2010-11-02