As we have claimed already, 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 3.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.

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.

In this chapter, we will discuss the role of each core plugin module, examine the operations which a replacement for the default must supply, and give observations about implementation as appropriate to each plugin.