Overview
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 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 (i) the behavior specification of the environment (e.g. the frame protocol of a target component), and (ii) 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.