# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 5 Discussion and Conclusions  
A new approach for modeling discrete time in Promela is presented. The previously known solution required a special version of Spin that do not include features from the recent versions of Spin, e.g., the inclusion of embedded C code for the ADT operators. We have compared DTMP to the DT Promela and DT Spin. Modeling of discrete time with the DT Spin is clear and simple. A timer is declared locally in a process. It is shown that complexity of formal verification with DT Spin is influenced directly by number of timers and their values. For qualitative properties, where correct ordering of events suffices, this can be optimized with the proposed fictitious-clock model of discrete time without silent events [33]. During the development of DTMP we were focused on modeling real-life SDL systems. DTMP is high-level Promela model for the SDL timer construct that is seamlessly integrated in our framework for modeling SDL systems and can be used with the mainstream version of the Spin tool. Therefore, its implementation is influenced by the rest of the Promela framework for modeling the abstract SDL machine. To the best of our knowledge, this is the only framework that supports a full SDL system structure, predefined and user-defined data types, dynamic process creation and termination, multiple process instances, timers with parameters, save construct, asterisk state, asterisk input, priority input, implicit transition, SAVE construct, rational numbers, enabling condition, direct and indirect addressing, path limitations, procedures and some other less frequently used SDL concepts. We stress that all of the listed constructs must be supported to model SDL specifications with implementation details. We have verified DTMP with complex SDL specification of an ISDN IUA protocol in [13], but further studies are necessary to check possible optimizations that would reduce the added complexity of this high-level solution. Our goal is to automate model extraction of real-life complex SDL specifications that include many timers with a great range of values without the need of manual abstraction of the timers. We have shown that DTMP is well suited for such systems, but we recognize that current research limitations include a low number of real-life specifications and lack of studies on large SDL systems (1 mio. lines of SDL code). Further research is necessary to explore the possible limitations of the method related to state space of the system and time needed for the formal verification of the model. The new activities within SDL standardization bodies and industry is motivating. Algorithms that are implemented in _sdl2 pml_ do not support [3] specifics. We are planning \begin{table}
\begin{tabular}{c c c c c c c c} \hline \hline \multirow{2}{*}{**Tool**} & \multicolumn{3}{c}{**Options and Parameters**} & \multicolumn{5}{c}{**Formal Verification Results**} \\ \cline{2-7}  & **Multiplier** & **Option** & **States** & **Transitions** & **State-Vector [B]** & **Memory [MB]** & **Time [s]** \\ \hline \multirow{8}{*}{**DT Spin 4.1.1** **(DT Promela)**} & 1 & POR & 632 & 690 & 48 & 1.253 & 0.000 \\ \cline{2-7}  & 10 & POR & 2612 & 2670 & 48 & 1.356 & 0.004 \\ \cline{2-7}  & 100 & POR & 22,412 & 22,470 & 48 & 2.911 & 0.016 \\ \cline{2-7}  & 1000 & POR & 220,412 & 220,470 & 48 & 18.341 & 0.176 \\ \cline{2-7}  & 10,000 & POR, INT & 2.2 \(\times\)\(10^{6}\) & 2.2\(\times\)\(10^{6}\) & 52 & 183.602 & 2.692 \\ \hline \multirow{8}{*}{**Spin 4.1.1** **(DTMP)**} & 1 & POR & 1005 & 1282 & 60 & 1.356 & 0.000 \\ \cline{2-7}  & 10 & POR & 1005 & 1282 & 60 & 1.356 & 0.000 \\ \cline{1-1} \cline{2-7}  & 100 & POR & 1005 & 1282 & 60 & 1.356 & 0.000 \\ \cline{1-1} \cline{2-7}  & 1000 & POR & 1005 & 1282 & 60 & 1.356 & 0.000 \\ \cline{1-1} \cline{2-7}  & 10,000 & POR & 1005 & 1282 & 60 & 1.356 & 0.000 \\ \cline{1-1} \cline{2-7}  & 100,000 & POR, INT & 1005 & 1282 & 68 & 1.356 & 0.004 \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Results for the Parallel Acknowledgment with Retransmission for DT Promela and DTMP.