5.2 PAT Class Diagram

5.2 PAT Class Diagram

Model checking involves functions like state-space exploration, process scheduling enumeration, and state management. In the actual implementation of existing model checkers, these functions are highly tangled in order to achieve optimal performance.

PAT is designed to allow reusing and extending the functions. We choose C# as the implementation language for the benefits of Object-Oriented design and competitive performance. By applying DESIGN PATTERNs [GAMMAHJV95], the implementation details are successfully hided with proper encapsulation. The coupling between the components is reduced and then extensibility can be achieved. We further apply this design strategy to module interface design. The dependency between common library and individual modules is minimized.

PAT's design is hierarchical, as reflected in the class diagram in the following figure. The system consists of two basic packages, namely PAT.GUI and PAT.Common, and 11 module packages. Each of the 11 modules implements necessary module interfaces and is packed into a plug-in DLL. The complete API can be found in section 5.4 PAT APIs.

We use the CSP module as a demonstrating example to explain the implementation details which involves implementation of GUI package & Common Package and Module Package in section 5.2.1 and 5.2.2 respectively.