We present a first report on our PARTS toolset for the automated static analysis of real-time systems. The PARTS toolset is based upon a timed extension of Petri nets.

Our simple time Petri nets or STP nets are specifically aimed at facilitating real-time analysis. Our analysis approach uses the state space of an STP net in order to answer queries about the concurrency and timing behavior of the corresponding system. An attractive feature of STP nets is that they support a variety of techniques for controlling the number of states that must be explicitly enumerated. These techniques were originally defined for the analysis of concurrency properties of untimed systems, and in this paper we discuss the extension of each to the timed domain.

We also report on some preliminary experimental results that we obtained by running our toolset on examples of real-time systems.