The Verification of Real Time Systems using the TINA Tool

In this paper, we propose a method for building a Timed Transition Graph (TTG) that uses a single clock from the state class graph of a bounded time Petri Net (TPN). To build this TTG a special state class construction - available in Tina - is used. This structure can be used to calculate “quantitative” temporal properties for the worst case scenario. It is possible to check efficiently several properties over the same TTG if no design modifications are made. Such properties are represented by a framework proposed in the literature were TCTL properties are defined on TPN.