![]() |
The easiest way of creating a model checker is to create a syntax rewriter
from a domain specific language to an existing language in PAT. This is only
recommended if the domain language is less expressiveness than the existing
languages. Comparing with other tools, programming a language translator is
straightforward in PAT. Because PAT has well-defined APIs for Specification
facade class and module language constructs, users only need to create the
Specification model and generate the language constructs objects using these
APIs. For example, Specification class in CSP# module offers the interfaces to
create global Variables, Channels, Processes and Assertions. This approach
requires little interaction with PAT codes. Most importantly, the target
language model is automatic generated from the Specification class, which can
guarantee syntax correctness. The usefulness of this extension has been
demonstrated by the build-in translator from Promela4 to CSP# [ZHAO10] and the translator from UML
state diagram to CSP# [ZHANGL10]. However, sometimes this approach will be infeasible. For example, the
translation may not be optimal if special domain specific language features are
present. In addition, reflecting analysis results (e.g., showing the
counterexample trace) back to the domain model is often
non-trivial.