Property Extension

PAT's design allows seamless integration of new model checking algorithms and optimization techniques. To create a new property, users need to create a new assertion class, inheriting the base Assertion class and implementing its methods. The dedicated model checking algorithm is implemented in the Verify method. In addition, method GetCounterExample must be implemented if a concrete counterexample is to be generated.
Note: that GetCounterExample is optional for some modules. For instance, for probabilistic model checking based on MDP, the verification result is a probability range, e.g., with more than 0.5 and less than 0.85 probability a property is satisfied, which may not require the generation of a counterexample.

PAT offers a number of algorithm templates like generic DFS and BFS algorithm to help the development of model checking algorithms. Furthermore, supporting functions, like LTL to Büchi or Rabin or Streett automata conversion which is essential for LTL model checking, or DBM library which is for real-time system verification, are provided in PAT. With the help of PAT's design, we have successfully extended PAT with the algorithms for divergence checking, timed refinement checking in real-time system module and new deadlock and probabilistic reachability checking recently.

Abstraction Extension

In general, abstraction techniques are to be encoded as part of language semantics, in the MoveOneStep or EncodeProcess methods of each language construct in each module. PAT offers a framework for abstract-refinement techniques. If over-approximation abstraction is applied, users must override the method to check whether a generated counterexample is spurious or not and override the method to re ne the abstraction.

Currently, PAT offers one module independent abstraction, i.e., process counter abstraction. Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/ concurrent systems. A common state space abstraction for checking parameterized systems groups behaviorally similar processes rather than keeping track of all process identifiers. When a system with identical concurrent processes, process counter abstraction can be implemented by invoking the library provided in PAT to update the counter and mark the group of identical processes as abstracted. The verification algorithms will automatically recognize this mark and check the generated counterexample is spurious due to the abstraction or real counterexample. With the provided sample code, process counter abstraction can be implemented quickly and correctly.