 Process
Analysis Toolkit (PAT) 3.5
Help |
Module Generator is to help developers to quickly build a new model checker
for any modeling language as a module of PAT. By providing module name, language
syntax construct names and choices of assertions, Module Generator automatically
generates the module project (in C#) with interface classes (e.g. ModuleFacade,
Specification, state interface etc.), language classes with code skeletons. With
the generated code, developers only need to create a parser of the new
modeling language and implement the operational semantics by completing the
specific methods within the code skeletons. A new module can be developed independently without the source code of PAT.
This approach is also 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. Users can find this
function under the Tools tab in PAT's editor, as shown in the
following figure. In this section, you can learn (1) in Section 5.4.1 how to use
Module Generator to generate a C# project for a new model checker, (2) in Section 5.4.2 how
to work with the generated code to complete the development of the target model
checker, and (3) in Section 5.4.3 an example of developing a
model checker for a simple language.
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.