EnvGen

Download

External dependecies

Publications

Environment Generator for Java PathFinder

Environment Generator is a tool that allows to create an environment for a primitive component that is necessary for verification of the component with the Java PathFinder. The need for an environment is caused by the fact that the Java PathFinder checks only complete Java programs and an isolated software component does not make such a program. Both the Fractal and SOFA component systems are supported.

The easiest way to use the tool is to create an instance of the EnvDescriptor class, set all fields of this object, and then pass the object to the generateEnvironment method of the EnvGen class. In particular, the tool has to get

  1. the behavior specification of the environment (e.g. the frame protocol of a target component)
  2. sets of possible values of method parameters (i.e. the name of a Java class that works as a container for the sets)

The getMainClassName method can then be used to get the name of a class that has the main method – name of this class should be supplied to the Java PathFinder.

The tool is developed and supported by Pavel Parizek.

Download

External dependencies

Publications

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 (3)

Refereed (journals/proceedings)

PDF Kofroň J., Adámek J., Bureš T., Ježek P., Mencl V., Parízek P., Plášil F.: Checking Fractal Component Behavior Using Behavior Protocols,
Presented at the 5th Fractal Workshop (part of ECOOP'06), July 3rd, 2006, Nantes, France, July 2006

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