# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 3 Discrete Time Model for Promela  
An SDL specification is comprised of different types of constructs which should all be supported by the selected formal verification environment. This article focuses on modeling the SDL timer construct. It is one of the SDL constructs that is not modeled easily with Promela, but is present in many SDL systems [29; 30; 31; 32]. A timer is an item owned by an process that causes a timer expiration signal to occur at a specified time at the input queue of the process [3]. In SDL TIME and DURATION are predefined data sorts with real values. In SDL real values can be presented by one integer divided by another, i.e., rational numbers. The origin of time is system dependent. TIME values are used to set the expiry time of timers. DURATION is used for the values to be added to timers and as the result of the difference between TIME values [2; 3]. Real numbers are abstracted with integers in the Promela model of the SDL system. Therefore, only the integer readings of the actual times with respect to a digital clock are recorded in the trace. DTMP implements a fictitious-clock where multiple ticks can be inserted between the events. It records the same order of the real-time events, but there are no silent events inserted between the events in the trace as they are in DT Promela [18; 33]. DTMP was inspired with the SDL notion of time, definition of timers, and its communication model. A timer in SDL is owned by a process instance and can be active or inactive. An active timer returns a timer expiration message to the owning process instance at a specified time. Each process can have multiple timers and process instances. In DTMP, each timer is assigned a unique Timer Identification Number (TID). Our framework supports dynamic creation of process instances. If a maximum number of instances is not defined in an SDL specification, we set it to 1 [34]. We acknowledge that this is not in accordance with [2], where the maximum number, if not defined, should be unbounded. Therefore, we encourage that the expected number of allowed instances are defined explicitly in the SDL description of the system. Figure 1 illustrates the basic idea of the DTMP. We have introduced a static Monitor process that manages all timers. A timer is declared as a signal with the unique TID that is defined globally with #define directive. Each process can include multiple definitions of timers. When a process activates a timer, it sends a message with TID and the value of the timer to the predefined rendezvous channel chan_timeout. This message can be extended with the optional timer parameters. The timer can be reset in a similar manner. Figure 1: Basic idea of Discrete Time Model for Promela. Time advances when no other statement within the system is executable. When the predefined Promela timeout event occurs the Monitor process sends messages to the input queues of all processes with expired timers. The input queue of the process instance is modeled with an associated Promela message channel. At each timeout event more than one timer can expire. This is in accordance with the SDL interpretation of timers and input queue management. DTMP extends an untimed Promela model with:  
1. some temporary variables,
2. the synchronous communication channel chan_timeout,
3. timer manipulation inline functions set and reset,
4. the Monitor process,
5. timer expiration inline function send_to_channel. Simple models can be prepared manually. Most of the DTMP functionality can be included with the dtmp.pml right before the prototype definitions. Only some macros and inline function send_to_channel has to be modified exclusively for each model of the SDL system. Contents of the dtmp.pml are shown in Listings 2 and 3. The TIMER_NUM_DATA_TYPE limits the number of available timers in the model to the range of the byte data type. This can be increased, if needed, but is best kept to a minimum range. It defines the size of the array of timers that is stored by the Monitor process. A timer is active if its value is greater than zero.