This approach is the most complicated compared with ones discussed previously. Nevertheless, this approach gives the most flexibility and efficiency. It is difficult to quantify the effort required to build a high-quality module in PAT. Experiences suggest that a new module can be developed in months or even weeks in our team. This approach is still feasible for domain experts who have only the basic knowledge on model checking, since model checking algorithms and state space reduction techniques are separated from modeling languages. In order to make use of the model checking library, only knowledge on the module interfaces and IRL is necessary.

To illustrate the feasibility of this approach, we elaborate the process of creating the TA module to support verification of Timed Automata models. The graphic interface for drawing Timed Automata is based on an existing module (e.g., the LTS module which allows users to draw LTSs). We omit the details here. Besides, creating this TA module involves 4 steps.

1. Create a package for the module and add the PAT.Common package in package's references (In the actual implementation, a package will be a C# project of type "Class Library". The output of the project is a single DLL file. PAT.Common package is a DLL, which can be found in PAT's installation folder).
2. Implement the module interfaces so that the module can be recognized by PAT. Module interfaces include two classes, i.e., ModuleFacade and Specification, which are the same as the CSP module shown in the class diagram.
3. Create a parser and the language related classes. The input language of TA module is a network of timed automata running in parallel. For each automaton, there are a set of states and transitions between the states. Because this modeling language is not hierarchical as CSP# (hence no need to apply COMPOSITE pattern), only one language syntax class is needed for the TA network and one class to store a single automaton. The global variables and channels can be implemented in the same way as CSP# module using Valuation class (refer to the Class Diagram). Clock variables and valuations can be implemented using Difference Bounded Matrix package provided by PAT.Common package. The expressions (variable assignments, guard conditions, etc.) can reuse the classes inside common package.
4. Connect with the intermediate layer by implementing the TAState. In TA module, each TAState should include the Valuation of global variables and channels, clock zones of type DBM and a TA network.

In total, users only need to implement 7 classes to create a module, i.e., 2 interface classes, 1 parser class, 3 language related components and 1 state interface. With the basic understanding of model checking and PAT tool design, we finish the TA module within a month.