PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

05, Sep, 2009: PAT 2.7.0 is released!

What’s new in PAT 2.7.0

In this release, the main achievement is that timed refinement checking algorithm is implemented in Real-Time System (RTS) module. At this stage, all the planned algorithms are implemented in RTS module. In the future, we will work on the syntax enrichment and performance improvement for RTS module. In this release, modeling languages in CSP and RTS modules are improved for better expressiveness power and parsing precision. Other updates include new examples and bug fixing.

Timed Refinement
Sometimes timing aspects are important in the system requirment, e.g., human heart must beat at rate between 50/minute to 200/minute (too low or too high is vital for human lifes). In these cases, we can use time refinement to check whether the input model follows the desired timing requirement. The syntax is the following:

#assert Implementation() refines< T> TimedSpec() ;

Note: For timed refinement checking, RTS module uses a timed trace semantics (i.e. a mapping from a model to a set of finite timed event sequences) and a timed trace refinement relationship (i.e. a model satisfies a specification if and only if the timed traces of the models are a subset of those of the specification). The verification algorithm developed for timed refinement checking will verify that a system model is consistent with a specification by showing a refinement relationship. A timed event sequence is presented as a counterexample if there is no such refinement relationship. For the timed refinement checking, PAT requires that the implementation or specifications are not divergent, otherwise the shared clock will not be bounded. If the system is divergent, PAT will ask user to provide a ceiling for the shared clock (default is 2^15).

Process Parameters are Supported in Grouped Processes
In order to have better compositional behaviors, we allow process parameters to be used in in grouped processes. For example, in []x:{0..n}@P or ||| {0} @ P() , n can be a global constant or process parameter, but not a global variable. We make this restriction for the performance reason. For example, the following definitions are all valid in PAT.
#define n 10; |||x:{0..n}@P;
P(n) = |||x:{0..n}@Q;

Channel Names can be Used as Event Names
Event name is an arbitrary string of form (‘a’..’z’|’A’..’Z’|’_’) (‘a’..’z’|’A’..’Z’|’0′..’9’|’_’)*. However, global variable names, global constant names, process names, process parameter names, propositions names can not be used as event name. One exception is the channel names are allowed, because we may want to use channel name in specification process to simulate the channel behaviors and use refinement checking to compare with real channel events.

Divergence-free
Given P() as a process, the following assertion asks whether P() is divergence-free or not.
#assert P() divergencefree;
Given a process, it may performs internal transitions forever without engaging any useful events, e.g., P = (a -> P) {a};, In this case, P is said to be divergent. Divergent system is ususally undesirable.

Timed Divergence-free
Given P() as a process, the following assertion asks whether P() is timed divergence-free or not.
#assert P() divergencefree< T>;
Given a process, it may performs internal transitions and timed transitions forever without engaging any useful events, e.g., Q = (a -> Wait[5]; Q) {a};, In this case, P is said to be timed divergent. Timed divergent system is undesirable, which can give unbounded timer, which disallows timed refinement checking.

Note: P = (a -> P) {a}; is divergent, but not timed divergent, because it performs internal transitions forever without timed transitions.

Others
1 User manual is updated to latest implementation.
2 Real-Time system examples (Timed PaceMaker) and timed refinement assertions are added.
3 Fix the bugs in parsing, GUI and other places.