PAT: Process Analysis Toolkit

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

RTS Module

In PAT, real-time systems are modeled using compositional timed processes. As to model the timed behaviors, instead of explicitly manipulating clocks, we dynamically create and prune clocks by implementing a number of timed behavior patterns such as delay, timeout, deadline, waituntil, timed interrupt, within, etc.

The following experiments shows 5 popular real time system models which is used by lots of model checkers such as KRONOS and UPPAAL. In the experiments, we reasoned about various behaviors about the real time systems such as deadlock freeness, mutual exlucsion, liveness and safety properties. Details are elaborated as follows:

—Fischer’s mutual exclusion protocol: The protocol is proposed by Fischer in 1985. Instead of using atomic test-and-set instructions or semaphores, mutual exclusion is guaranteed by carefully placing bounds on the execution time of the instructions, leading to a protocol which is simple and relies heavily on time aspects. The property is mutual exclusion.

—Railway control system: A railway control system controls trains passing a critical point such as a bridge. The idea is to use a computer to guide trains from several tracks crossing a single bridge instead of building many bridges. Obviously, a property of such a system is that a train always eventually passes the bridge.

—CSMA/CD protocol: This protocol describes a solution to the problem of assigning the bus to only one of many competing stations arises in a broadcast network with a multi-access bus. The property is that a collision is always eventually detected. The model is based on the one in KRONOS [BDM+98], extended to arbitrary number of stations.

—Fiber Distributed Data Interface (FDDI): FDDI is a high-performance fiber-optic token ring local area network. An FDDI network is composed by N identical stations and a ring, where the stations can communicate by synchronous messages with high priority or asynchronous messages with low priority. The property is that the token cannot be in two stations simultaneously which is the safety property.

— Timed Pacemaker: Pacemaker is a small device placed in the chest or abdomen to help control abnormal heart rhythms. It’s critical real time application that with a complex hierarchical structure that is deemed to be too complicated to be modeled in Timed Automata, while it is feasible for PAT to model it. A simple property is that the pacemaker is deadlock-free.

Experiment results are shown in the table below. Here Time_zeno means that the property is verified with non-Zenoness check. We also done the comparison work with UPPAAL, and here UPPAAL-r means a revised version of its original models with some τ -transitions to make them consistent with our PAT model.

From the experiments, we can see that PAT Real Time System Module can handle a rich set of properties within reasonable time. Also, a number of observations are here: Firstly, PAT currently handles in average 13, 000 states per second (i.e., the total number of visited states – not new states – divided by the total number of seconds), which is comparable to existing model checkers. Secondly, model checking with non-Zenoness has little or no computational overhead in PAT. Thirdly, PAT is considerably slower than UPPAAL. A number of reasons might account for why UPPAAL outperforms PAT. For instance, system configurations in PAT are more complicated than those in UPPAAL as Stateful Timed CSP is designed for hierarchical complex systems. The main reason is that UPPAAL has benefited from many dedicated optimization techniques such as extrapolation, however PAT has none yet. The experiment data is available here.