# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 2 Related Work  
[PERSON], author of the Spin tool, presented an experiment of validating SDL specifications with Supertrace, the predecessor of the Spin tool [21]. It provided an automatically generated model of an SDL specification. Timers were modeled with Promela processes that took only subclass of timer behaviors into account. Timeout was considered as a possibility that is either present or absent without relative timings in the system. Later, Supertrace was integrated into the tool Sdlvalid [22]. In [11] [PERSON] and [PERSON] provide formal semantics for untimed Spin and introduce formal semantics for Real-time Promela (RT Promela). An example of a quantitative property, that can be checked independently of a specific time unit (dense time), is: \"between event A and event B at least 5 time units should pass\" [23]. Their verification method consists of considering the emptiness of a Buchi automaton that is extended with a finite number of clocks. RT Promela introduces globally declared clock variables that could be scalars or arrays. Each statement can be expanded with an optional time part that acts as a guard. A detailed description is out of the scope of this article, but it should be noted that this method was implemented as an extension to the Spin tool, with additional object files which implement the symbolic operations on difference bound matrices representing real-time information. [PERSON]'s mutual exclusion protocol was used as one of the examples to demonstrate the use of RT Promela [11]. As was pointed out in [24], RT-Spin is not compatible with the partial order reduction algorithm. The tool is not available for Spin versions later than 2.0. Therefore, we did not investigate its applicability to the models of the SDL systems. [PERSON] presented his ongoing research on Real-time model checking based on timed graphs that would support verification of quantitative aspects of real-time systems at Spin Workshop [25], but we are not aware of any available Spin extensions that would implement this research. [PERSON] presented modeling of Nokia Telecommunications SDL (NTSDL), which is a dialect of the SDL [26]. Timers are modeled by the process that receives all requests for the SET statements. Upon the reception of the request, it sends a timer expiration message back immediately to the activating process. RESET statement is a procedure that removes the message associated with the timer expiration from the buffer of the timer process and the activating process. [PERSON] and [PERSON] integrated support for Discrete Time Promela into prototype version of Spin [18; 24]. The DT Spin tool is intended for verification of concurrent systems that depend on timing parameters. It allows quantification of the time elapse between events, by specifying the time slice in which they occur. In DT Promela, statements of a process are divided into time slices by putting set and expire at the beginning and the end of the time slice. The application of DT Promela and DT Spin to model checking SDL systems is presented in [12]. It is a two-step process. First, the SDL system is translated to Intermediate Format (IF) with the tool sdl2 if that was part of the commercial ObjectGEODE tool which became unavailable [27; 28]. Some SDL constructs, e.g., enabling condition and continuous signals, are transformed to more primitive constructs. Furthermore, it does not support dynamically created processes and ADT. All mentioned shortcomings are overcome in our Promela framework for SDL systems. In the second step the if2 pml tool is used to perform the translation to DT Promela. In DT Spin, time is divided into slices of equal length and indexed by natural numbers. The elapsed time is measured in ticks of a global digital clock that is increased only when all processes have finished execution of their actions for the current time slice [24]. That is accomplished with the use of predefined Promela statement timeout that becomes true when no other statement within the system is executable.