Bogor Website - Bogor Architecture

1. Overview

As we have claimed, Bogor was designed with modularity as the highest goal. Each separate logical function of a model checker is isolated and contained behind an abstract interface. In Figure 1, “Bogor Architecture�?, the nine primary portions of Bogor are shown. Each core module is implemented as a plugin. The arrows denote inter-module dependencies; e.g., the ISearcher plugin uses the IStateManager and IStateFactory modules to assist in the performance of its assigned task: the state-space exploration algorithm.

Figure 1. Bogor Architecture

This is a fine goal to claim. Does Bogor really achieve independence of implementation for each module, or do modules covertly make assumptions about the actual classes implementing neighboring plugins? One measure of the degree in abstraction (or lack thereof) is to determine where the class signature of each default plugin implementation is used. For instance, does the default ISearcher silently downcast the reference to its IStateManager into a DefaultStateManager? Using the "References" feature of Eclipse's Java IDE, it is a short task to find all uses of the DefaultStateManager in the Bogor source code. There are none outside the definition of the class itself; the same holds true for each default module implementation in Bogor. Only the contract stipulated in each module's interface matters.

We must admit to one caveat. Some users who wish to customize Bogor to a domain may have good reason to introduce inter-module coupling. A particular state-space exploration algorithm may require some extra state management features not supplied by the standard IStateManager interface. While users are highly encouraged to make their plugins orthogonal to the rest of Bogor's functionality, this constitutes a legitimate special-case use of the framework. The core Bogor development team has, for instance, written a special search algorithm (ISearcher) for simulation of real-time execution which require a specialized IStateFactory capable of making states which contain extra scheduling information.

2. Module Initialization

A fully loaded and operating Bogor "virtual machine" consists of numerous semi-independent objects, all inheriting from IModule. Normally, each of these will be an object providing a concrete implementation of exactly one of the abstract model checking components of Bogor (for example, IValueFactory and IBacktrackingInfoFactory from Figure 1, “Bogor Architecture�?). Some of the modules are also "free-floating;" rather than occupying fixed positions in the architecture, they are loaded as requested by the user to provide the implementations of extension datatypes or contribute custom handlers for events generated by Bogor's internal signal/callback mechanism.

Before all these modules can cooperate at runtime, they must be allocated and initialized. A single IBogorConfiguration object serves as the container for the entire Bogor runtime environment. There are three phases which occur inside this container's initialize() method: allocation, configuration, and connection.

2.1. Allocation

The first step of initialization, allocation, requires the IBogorConfiguration to consult the key/value configuration file to fetch classnames for each model checking component. After each classname is retrieved, a series of attempts are made to allocate a singleton instance of each distinct IModule class. If any of these attempts fails, then an error message is reported back to the main() routine and initialization is aborted.

Note that the name of the various IModule classes which provide extension operation implementations are not obtained from the configuration file, but rather the BIR module directly in the extension declaration. The appearance of the following declaration: extension Foo for myPackage.FooModule would cause Bogor to attempt instantiation of one myPackage.FooModule object.

One pathological case would be the re-use of a Java class to provide implementations of multiple model checking components or language extension components. In this case, only one copy of the module is allocated. The single instance is re-used for each role that the class assumes.

2.2. Configuration

After all components are allocated, initialize() gives each an opportunity to read the user-provided configuration. The setOptions() method of each module is called in turn. Each module is here expected to extract the relevant portions of the configuration (for example, the searcher typically reads only those configuration entries whose keys begin with edu.ksu.cis.projects.bogor.module.ISearcher). If some option is nonsensical or malformed, then the module issues a warning or error message (as a FileMessage object).

Figure 2. Example configuration of module options

          
/**
 * Configuration option name
 */
public static final String USE_OPTIMIZATION_ID = "useOptimization";
  
/**
 * Optimizations enabled by default
 */
protected boolean useOptimization = true;

public IMessageStore setOptions(String key, Properties options)
{
    String useOptimizationId = key + "." + USE_OPTIMIZATION_ID;
    
    ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
    ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();
      
    for (Iterator<Object> i = options.keySet().iterator(); i.
        hasNext();)
    {
        String optionId = (String) i.next();
        String value = options.get(optionId);
        
        if (useOptimizationId.equals(optionId))
        {
            // Check for well-formedness
            String trimmed = value.trim().toLowerCase();
            
            if (trimmed.equals("true") || trimmed.equals("false"))
            {
                // If legal form, then configure option
                useOptimization = trimmed.equals("true");
            }
            else
            {
                // If malformed, then report an error. This will prevent
                // model checking.
                errors.add(FileMessage.buildMessage(
                    optionId,
                    ConfigurationMessage.BAD_FORMAT,
                    new String[]
                        {
                            optionId, "boolean", value
                        }));  
            }                        
        }
        else if (optionId.startsWith(key) && !optionId.equals(key))
        {
            // Issue a warning that some option beginning with the fully
            // qualified module name which this component fulfills, has been
            // unexpectedly specified.
            warnings.add(FileMessage.buildMessage(
                optionId,
                ConfigurationMessages.UNKNOWN_OPTION,
                new String[]
                    {
                        optionId
                    }));
        }
    }
    
    return new DefaultMessageStore(errors, warnings);
}

Warnings are considered informative only, but if any module issues an error, initialization will halt after this second phase.

2.3. Connection

The connection phase is the final step toward bringing a Bogor virtual machine to readiness. In this step, links between model checking components are established. This is accomplished by calling connect() in sequence on each of the IModules. The default implementation of IExpEvaluator, for example, acquires references to the scheduler and value factory components.

The normal lifecycle of a model checker component indicates that references acquired during the connect() method should be released during the accompanying dispose() method.

As with the configuration phase, each module finishes its connection step by returning a collection of error and warning FileMessages. If any error is reported, the model is considered not well-formed and model checking does not occur.

Figure 3. Excerpts from reference acquisition phase of expression evaluator component

          
/**
 * Snippets from the default implementation of the IExpEvaluator
 * interpretative component.
 */
public class DefaultExpEvaluator implements IExpEvaluator // (implicitly implements IModule)
{
    /**
     * Reference to another model checking component. Used to create
     * value objects encoding results of evaluating BIR expressions.
     */
    protected IValueFactory vf;
    
    /**
     * Reference to another model checking component. Used to assist in
     * systematically traversing nondeterministic choices during expression
     * evaluation.
     */
    protected ISchedulingStrategist ss;
    
    ...
    
    /**
     * Acquire references to runtime components.
     *
     * @param bc
     *           the Bogor "virtual machine". All the important data structures
     *           and runtime modules are accessible from here
     */
    public IMessageStore connect(IBogorConfiguration bc)
    {
        this.vf = bc.getValueFactory();
        this.ss = bc.getSchedulingStrategist();
        
        ...
        
        // No errors are really possible here, so just return empty
        // set of messages.
        return new DefaultMessageStore();
    }
    
    /**
     * Drop references to runtime components and other data structures.
     */
    public void dispose()
    {
        this.vf = null;
        this.ss = null;
        
        ...
    }
}