ions for ITPNs suitable to verify reachability, linear and branching properties, in addition to a TCTL model checker. In this paper we describe the ITPN model as a proposed extension to the classical TPN model and describe the modular modeling capabilities of RT-Studio. The classical railroad crossing model is used to illustrate these capabilities.
Interpreted Time Petri Nets (ITPNs) are Time Petri Nets (TPNs) [
In the field of realtime systems modeling and verification, UPPAAL is one of the
best tools available [
For the TPN model, many tools exist for modeling, analysis and verification. Some
well known tools are Roméo [
To increase the modeling power and expressiveness of TPNs , we extended the TPN model with bounded integer variables and associate guards and update actions with transitions. The resulting model is called Interpreted TPN (ITPN). As a consequence, in addition to the normal transition firing requirements, a transition requires also that its guard is true in the current ITPN state. A guard is a condition on the ITPN state defined on its marking, firing intervals of transitions, and the state of associated variables. After a transition t is fired, associated updates are performed. Updates can target variables associated with the ITPN, but also its marking. An update can only target places not attached to t for not conflicting with the usual operational semantics of transition firing. With the new extension, inhibitor arcs and priority on transitions firing can be modeled. Note that if variables associated with an ITPN are always positive then they can be implemented as normal places.
Let Q+, R+ and Z be respectively the set of positive rational numbers, the set of positive real numbers and the set of integers. Let Q[+] be the set of non empty intervals of R+ which bounds are respectively in Q+ and Q+ ∪ {∞}. For an interval I ∈ Q[+], ↓ I and ↑ I denote respectively its lower and upper bounds.
An ITPN P is a tuple (P, T, V, P re, P ost, m0, v0, Is, G, U ) where: – P is a finite set of places, – T is a finite set of transitions, withP ∩ T = ∅, – V is a finite set of integer variables, with(P ∪ T ) ∩ V = ∅, – P re and P ost are respectively the backward and forward incidence functions: P ×
T → N, where N is the set of nonnegative integers, – m0 : P → N, is the initial marking, – v0 : V → Z, is the initial valuation on P variables. – Is : T → Q[+] associates with each transition t an interval [↓ Is(t), ↑ Is(t)] called its static firing interval. The bounds ↓ Is(t) and ↑ Is(t) are called the minimal and maximal static firing delaysof t. – G : T → Bool(P), associate with each transition a guard from the set Bool(P).
Bool(P) is the set of boolean functions on the set SP of states of P (The ITPN state is defined next). – U : T → U pdate(P), where U pdate(P) is the set of integer functions on the set SP × (P ∪ V ), associates with each transition t an update function on places and variables associated with P.
Let M be the set of all markings of P. Let m ∈ M be a marking, and t ∈ T a transition of P. t is said to be enabled in m, iff all tokens required for its firing are present in m, i.e.: ∀p ∈ P, m(p) ≥ P re(p, t). We denote by En(m) the set of all transitions enabled in m. If m results from firing transition tf from another marking, N ew(m, tf ) denotes the set of all newly enabled transitions in m, i.e.: N ew(m, tf ) = {t ∈ En(m)|∃p, m(p) − P ost(p, tf ) < P re(p, t)}.
Definition 2. ITPN state
The state of ITPN P is a couple (m, v, I), where m is a marking, v is a valuation on
the variables of P, and I is an interval function I : En(m) → Q[+] [
For a state s = (m, v, I), and t ∈ En(m), I(t) is called the firing intervalof t. It is the interval of time where t can fire. The initial state ofP is s0 = (m0, v0, I0), where I0(t) = Is(t), for all t ∈ En(m0). The state of P evolves either by time progression or by firing transitions. When a transitiont becomes enabled, its firing interval is set to its static firing intervalIs(t). The bounds of this interval decrease synchronously with time, until t is fired or disabled by another firing.t can fire, if the lower bound ↓ I(t) of its firing interval reaches0 and its guard G(t) evaluates to true in the current state of P, but must be fired, without any additional delay if the upper bound↑ I(t) of its firing interval reaches 0 while its guard evaluates true. The firing of a transition takes no time.
Let s = (m, v, I) and s0 = (m0, v0, I0) be two states of P. We write s →θ s0, iff state s0 is reachable from state s after a time progression of θ time units (s0 is also denoted s + θ), i.e.: ∃θ ∈ R+, Vt∈En(m) θ ≤ ↑ I(t),
m0 = m, v0 = v, ∀t0 ∈ En(m0), I0(t0) = [max(↓ I(t0) − θ, 0), ↑ I(t0) − θ].
We write s →t s0 iff state s0 is immediately reachable from state s by firing transitiont. i.e.: t ∈ En(m), ↓ I(t) = 0 ∧ G(t, s) = true, m0(p) = m(p) − P re(p, t) + P ost(p, t) if P re(p, t) 6= 0 ∨ P ost(p, t) 6= 0, ∀p ∈ P m0(p) = U (t, s, p) otherwise, ∀x ∈ V, v0(x) = U (t, s, x), I0(t0) = Is(t0) if t0 ∈ N ew(m0, t), ∀t0 ∈ En(m0) I0(t0) = I(t) otherwise.
The state space of an ITPN model P is the structure (S, →, s0), where: – s0 = (m0, v0, I0) is the initial state of P, – s → s0 iff either s →θ s0 for some θ ∈ R+ or s →t s0 for some t ∈ T , – S = {s|s0 →∗ s}, where →∗ is the reflexive and transitive closure of →, is the set of reachable states of P. 3
RT-Studio uses the concept of programming project2 to allow for a modular design of a realtime system. A project is basically a collection of ITPN components, and a system description file. An ITPN component is actually a template with possible parameters. The system description file is where the system configuration is specified. It consists of a list shared variable declarations and instantiations of ITPN components.
Instances of ITPN components within the same project can communicate and synchronize using data variables defined in the system description file, and using shared transitions and shared places. A transition or a place is shared between several ITPNs if it has the same name and set as external (not local) in each one of them. When synchronizing ITPN components instances, shared places with the same name are merged in one single place. The marking of that place is the maximum marking of synchronized places. For transitions, the synchronization is little bit more demanding. A transition meant for synchronization is implicitly associated with a signaling channel having the same name. Transitions which names end with and exclamation mark ’!’ represent send actions on associated channels. Those with names ending with an interrogation mark ’?’ represent receiving actions on associated channels. When instances of ITPN components are synchronized, transitions representing complimentary actions are synchronized by merging each sending transition with a copy of a receiving transition having the same name. A copy of a transition is created by duplicating the transition and all its ingoing and outgoing arcs.
Each ITPN component element (place, transition, arc), including the ITPN itself has an extendable list of attributes (properties). When an ITPN component or an ITPN component element is created, a default list of attributes is associated with it. These attributes describe its different features, like the number of tokens for a place, the guard and update actions for a transition, the list of parameters for the ITPN component,
including the visual appearance of ITPN elements like the color, the shape, the border size, etc. The Attribute viewer is a panel for editing, modify and adding new attributes for the currently selected ITPN element. Added attributes can be referred to in guards and updates actions of transitions. Three attribute types are supported in the current version of RT-Studio: number (real value), boolean and string.
To analyze a system designed as a project, its system description file need to be compiled. The compilation consists in synchronizing all ITPN components instances in one single ITPN. In the case of any error, error messages are displayed in a message pane at the bottom of the main window, otherwise the synchronized ITPN is generated and displayed in a separate panel and ready to be analyzed if it is self contained3. Note that a self contained ITPN components can be analyzed without compilation. 4
RT-Studio’s verification and analysis capabilities can be grouped in three categories:
abstract state spaces construction, model checking and simulation. Both known
characterizations of the TPN state (interval and clock characterizations) [
ITPNs.
during the simulation if needed. RT-Studio stores a project in a single XML file. It also
allows to import or export self contained ITPNs to a text file in a simple format accepted
by the TINA toolbox [
in
2 2 exit far m app
coming As an illustrative example, we consider the classical Railroad Crossing model. Components of this system are shown in Figure 1 and also in Figure 2 as screen shots from RT-Studio. The ITPN model of n trains crossing concurrently the road is obtained by synchronously composing the controller model with its parameter m4 set to n, the barrier model, and n instances of the train model. In Figure 2, we can see the system description file for the railroad crossing project where two instances of the train model (Train1 and Train2) are synchronized with one instance of the barrier model (Barrier) and one instance of controller model (Controller). After compiling the project, we obtain the synchronized ITPN of the whole system shown in Figure 3. Note that for clarity, in Figure 3 each transition app is actually the superposition of two app transitions; one synchronized with first train instance, the other one with the second train instance. At the right bottom of Figure 2, we can see the SCG of the synchronized ITPN computed by RT-studio.
RT-Studio can be downloaded from http://faculty.qu.edu.qa/rhadjidj/rt-studio.aspx. The tool comes in a Zip file that includes three files :RT-studio.jar, realtime.exe, readme.txt, and a directory for examples. RT-studio.jar is a Java executable representing the graphical interface of the tool. realtime.exe is the engine written in C++ for performance. Installing the tool consists in simply unziping the zip file in chosen directory. Double clicking on the fileRT-studio.jar launches the tool.
On the download web page there are video tutorials that explain how to install and use the tool to model, simulate and verify properties.