After some testing, PAT 3.0 is arrived. Compared with the beta version, we mainly do the bug fixing.

New features in the RTS module:
Urgent Event

In RTS module, we assume all the event prefix, data operation and channel communication (channel input/channel output) takes arbitrary amount of time. Sometimes, we want the events takes no time (instantaneous events). The normal approach is to use (Process within[0]) to model this requirement. In RTS module, we introduce the concept of Urgent Event to simplify this kind of modeling. The supported syntax is shown in the following examples.

event{program} ->> Process

c!x ->> Process

c?x ->> Process

Note: tau event in RTS module is an urgent event by default. A natural consequence is that, all events after hiding become tau event and take no time.

Timed Zenoness Checking

Because RTS module supports process constructs like deadline, it suffers from zeno executions, i.e., infinitely many steps taking within finite time. Zeno executions are unrealistic and therefore must be ruled out in model checking. It is known that zone graphs are not fine enough to distinguish zeno executions. We show that the zone graph produced by dynamic zone abstraction can be modified so that the properties are verified with the assumption of non-Zenoness.

To remove zeno executions, PAT implements Zeno checking for LTL/Deadlock assertions. Users only need to tick the “Apply Zeno Check” in the model checking form. More Zeno checking will be implemented for RTS module.