Model Checking of WebRTC Peer to Peer System

  •  Asma El HAMZAOUI    
  •  Hicham BENSAID    
  •  Abdeslam EN-NOUAARY    


The establishment of the multimedia session is crucial in the WebRTC architecture before media and data transmission. The preliminary bi-directional flow provides the network with all the information needed in order to control and manage the communication between end-users. This control includes the setup, management, and teardown of a session and the definition, and the modification of multiple features that will be enabled in the ongoing session. This is performed by a mechanism named Signaling. In this work, we will use the formal verification to increase confidence in our SDL model by checking the consistency and reliability of the WebRTC Peer to Peer system. The verification and validation are proved the most efficient tools to avoid errors and defects in the concurrent system designs. Indeed, by using model-checking techniques we will verify if the WebRTC system adheres to standards if it performs the selected functions in the correct manner. To achieve that, we will first translate the SDL model to an intermediate format IF that will be retranslated to a Promela Model. Second, using the SPIN model checker, we will verify the general correctness of the model before checking if the desired properties are satisfied using the Linear Temporal Logic (LTL).

This work is licensed under a Creative Commons Attribution 4.0 License.
  • ISSN(Print): 1913-8989
  • ISSN(Online): 1913-8997
  • Started: 2008
  • Frequency: quarterly

Journal Metrics

WJCI (2020): 0.439

Impact Factor 2020 (by WJCI): 0.247

Google Scholar Citations (March 2022): 6907

Google-based Impact Factor (2021): 0.68

h-index (December 2021): 37

i10-index (December 2021): 172

(Click Here to Learn More)