5.1 PAT Architecture

5.1 PAT Architecture

In our PAT framework, we adopt a layered design with an intermediate representation layer (IRL), which separates modeling languages from model checking algorithms. Hence these algorithms (or other analysis techniques like testing) can be shared by different languages. As shown in the figure below, PAT's architecture has four layers, which split the model checking process into three steps: compilation,abstraction and verification. This separation reduces the coupling between different functionalities, hence increases the reusability of lower layers and the extensibility of upper layers. The four layers are introduced in the following:

Modeling Layer
Modeling layer contains modules of the supported application domains (e.g., distributed system, service oriented computing, security protocols and so on). It identifies the domain specific language syntax, well-formness rules as well as formal operational semantics, which are all encapsulated in a separate module. Two key components which are the language parser and model components (including syntax classes, variables, channels, etc.) consists this layer.

Abstraction Layer
Since model checking techniques only work with finite state systems, while a system often has infinitely many states according to its concrete operational semantics, that (automated) state abstraction is essential. In this layer, we applied abstraction technique into systems. For instance, zone abstraction abstract infinite TTSs into finite ones, process counter abstraction to group identical processes using process counter variables and ignore process identifiers (if they are irreverent) which reduces state space significantly. Partial order reduction to reduce all possible interleave execution orders of parallel running processes into a particular execution order is another effective method.

Intermediate Representation Layer (IRL)
After compilation and abstraction, the input model is converted to some form of internal representations, which is the basis of the model checking algorithms. Intermediate representation layer contains different semantic representations for different model checking approaches.

For explicit model checking, three configuration interfaces are defined, i.e., LTS- the most general semantic models for untimed systems, TTS- the common semantic model for Timed Automata and timed process algebras, and MDP- for probabilistic systems. Each of the interfaces has a number of operations, which allow the underlying model checking algorithms (such as methods: MoveOneStep and GetID) to drive the execution of the system and collect information from system states. The configuration interface can also be used by the simulator to show the system state space graphically.
For symbolic model checking, different operations are defined capture the language semantics, e.g., in the form of Boolean formulae. The Boolean formulae are usually stored in the form of Binary Decision Diagram (BDD) for symbolic model checking or Conjunctive Normal Form (CNF) for bounded model checking. For BDD-based symbolic model checking, a method EncodeProcess is defined for each language construct.

Analysis Layer (IRL)
This layer contains reusable model checking algorithms. For each intermediate representation in IRL, a set of algorithms are developed. For example, deadlock checking, reachability checking, LTL verification with or without fairness assumptions, refinement checking have been developed for LTS. If the verification result is false, a counterexample is produced, which can be visualized via simulator.