Modeling and Verification of Call Setup Dynamics of LTE Communication Systems

The Long Term Evolution (LTE) is the latest protocol for 4th generation of mobile communication systems that has integrated everything over the Internet Protocol. LTE is a very complex communication system at each layer of communication. Formal methods use mathematical language to explicitly specify system specifications and requirements that eventually help us to develop a reliable, scalable and complete software system. In a communication system like LTE, connection components and resource management parameters can be efficiently handled using discrete mathematical structures. In this paper, we have presented the static and dynamic model of LTE call setup using Z specification language. All the schemas generated through Z language are verified by using Z/Eves toolset. The aim of our research is provide a sound mathematical foundation for call setup system validation and verification.