# Discrete Time Model for Process Meta Language with Fictitious-Clock
## 1 Introduction  
Telecommunication systems consist of heterogeneous nodes. They are controlled by different microcomputer systems running programs that were developed in various programming languages. Due to many concurrent activities, they usually describe complex behaviors. Checking of the correctness properties of such systems is not a trivial task. Therefore, use of formally-defined languages is recommended for specification of such systems. Specification and Description Language (SDL) is one of the leading domain specific languages [1] that is defined formally by international Standards [2; 3; 4; 5; 6] and well-established in industries like telecommunications, medical, automotive, military, avionics, aerospace, internet of things, system engineering [7], and others [8; 9]. Versions SDL'88 and SDL'92 are used by our industry partner Iskratel d.o.o. for formal specification of concurrent, reactive, and distributed systems, e.g., MG6114 AX (Media Gateway), IC1020 AX (IMS Core), CS6116 AX (Call Server, Unified Communications), IE1020 AX (IMS Edge), IA1020 AX (IMS AS), and CE6111 AX (Compact Call Server). The SDL system specifications describe the implementation details and are used to build the production systems. Such specifications contain SDL constructs and additional extensions that enable developers to include operators that are implemented in other programming languages. The C programming language is used for low-level or processorintensive operations. We work mostly on semi-formal specifications of telecommunication systems, since parts of the system consist of Abstract Data Type (ADT) operators written in C. Formal verification with the model checking technique can help improve the reliability of such systems. It can check automatically if the model of the system is in accordance with the system's requirements. Formal verification can be performed by many software tools. We selected a Spin (Simple Promela Interpreter) tool [10]. It is a software package for verification of complex concurrent and reactive systems. The model of the system is described in a high-level language, named Promela (Process Meta Language). Like SDL, Promela adopts the strong formal basis established in ECFSM (Extended Communication Finite State Machine). Such systems consist of a finite number of separate components, which act independently one from another, and interact through the exchange of messages over message channels, or by memory sharing, via global variables. Message passing can be buffered or unbuffered (rendezvous channel). Concurrency is asynchronous and modeled by interleaving. There are no assumptions made on the relative speed of the process executions [11; 12]. Properties can be checked with assertions, accept label, progress label, or LTL (Linear Temporal Logic) formula that is translated automatically to never-claim. The never-claim process is Buchi Automata, and can express \(\omega\)-regular properties. If a system violates a property, Spin provides a counterexample, i.e., an execution path that violates the property. Model checking of a complex SDL system is comprised of many steps. First, a model of the system must be prepared. It could be constructed manually or extracted with some (semi)automated process. The latter requires less-knowledge verification engineers and is much faster, especially for comprehensive SDL specifications. Research is motivated by the need of the industry for the formal verification of the SDL systems that are in production but are still actively developed or fine-tuned to the various local requirements of the telecommunication markets. The 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. Our research focuses on a semi-automated approach. Before the automated extraction of the model is used, environment of the SDL system should be modeled to provide the behavior that is required to check the requirement specification successfully [13].