Formal verification of a peer-to-peer streaming protocol
Peer (P2P) networks have emerged as an efficient and affordable means of transmitting videos to numerous end-users via the Internet. The dynamic and heterogeneous nature of P2P streaming systems (P2PSS) makes testing, analyzing and verification a cumbersome task. However, formal methods offer effici...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Elsevier
2020-07-01
|
| Series: | Journal of King Saud University: Computer and Information Sciences |
| Subjects: | |
| Online Access: | http://www.sciencedirect.com/science/article/pii/S1319157818304245 |
| _version_ | 1818441859570073600 |
|---|---|
| author | Oluwafolake E. Ojo Ayodeji O. Oluwatope Suraju O. Ajadi |
| author_facet | Oluwafolake E. Ojo Ayodeji O. Oluwatope Suraju O. Ajadi |
| author_sort | Oluwafolake E. Ojo |
| collection | DOAJ |
| description | Peer (P2P) networks have emerged as an efficient and affordable means of transmitting videos to numerous end-users via the Internet. The dynamic and heterogeneous nature of P2P streaming systems (P2PSS) makes testing, analyzing and verification a cumbersome task. However, formal methods offer efficient approaches to rigorously analyze and verify P2PSS. This paper demonstrates the use of formal verification techniques for analyzing the behavioral properties of P2PSS. We use temporal logics to analyze whether all the possible behaviors within the P2P streaming systems conform to the defined specifications. Specifically, we apply model checking to check the consistency, completeness and certainty of the model if the temporal properties of the proposed system satisfies the required specifications. Furthermore, the P2PSS framework was modeled and verified using Simulink Design Verifier (SDV) in MATLAB simulation tool. The simulations results showed 100% validation for all frames and 50% validation for I-frames prioritisation. Further, the probability of a peer capable of forwarding frames while receiving is at most 0.5. |
| first_indexed | 2024-12-14T18:34:57Z |
| format | Article |
| id | doaj.art-619dc81058a34449b903cfe874db2fa4 |
| institution | Directory Open Access Journal |
| issn | 1319-1578 |
| language | English |
| last_indexed | 2024-12-14T18:34:57Z |
| publishDate | 2020-07-01 |
| publisher | Elsevier |
| record_format | Article |
| series | Journal of King Saud University: Computer and Information Sciences |
| spelling | doaj.art-619dc81058a34449b903cfe874db2fa42022-12-21T22:51:39ZengElsevierJournal of King Saud University: Computer and Information Sciences1319-15782020-07-01326730740Formal verification of a peer-to-peer streaming protocolOluwafolake E. Ojo0Ayodeji O. Oluwatope1Suraju O. Ajadi2Department of Computer Science, Federal University of Agriculture, Abeokuta, Nigeria; Corresponding author.Department of Computer Science and Engineering, Obafemi Awolowo University, Ile-Ife, NigeriaDepartment of Mathematics, Obafemi Awolowo University, Ile-Ife, NigeriaPeer (P2P) networks have emerged as an efficient and affordable means of transmitting videos to numerous end-users via the Internet. The dynamic and heterogeneous nature of P2P streaming systems (P2PSS) makes testing, analyzing and verification a cumbersome task. However, formal methods offer efficient approaches to rigorously analyze and verify P2PSS. This paper demonstrates the use of formal verification techniques for analyzing the behavioral properties of P2PSS. We use temporal logics to analyze whether all the possible behaviors within the P2P streaming systems conform to the defined specifications. Specifically, we apply model checking to check the consistency, completeness and certainty of the model if the temporal properties of the proposed system satisfies the required specifications. Furthermore, the P2PSS framework was modeled and verified using Simulink Design Verifier (SDV) in MATLAB simulation tool. The simulations results showed 100% validation for all frames and 50% validation for I-frames prioritisation. Further, the probability of a peer capable of forwarding frames while receiving is at most 0.5.http://www.sciencedirect.com/science/article/pii/S1319157818304245Peer-to-peer networksVideo streaming and temporal logic |
| spellingShingle | Oluwafolake E. Ojo Ayodeji O. Oluwatope Suraju O. Ajadi Formal verification of a peer-to-peer streaming protocol Journal of King Saud University: Computer and Information Sciences Peer-to-peer networks Video streaming and temporal logic |
| title | Formal verification of a peer-to-peer streaming protocol |
| title_full | Formal verification of a peer-to-peer streaming protocol |
| title_fullStr | Formal verification of a peer-to-peer streaming protocol |
| title_full_unstemmed | Formal verification of a peer-to-peer streaming protocol |
| title_short | Formal verification of a peer-to-peer streaming protocol |
| title_sort | formal verification of a peer to peer streaming protocol |
| topic | Peer-to-peer networks Video streaming and temporal logic |
| url | http://www.sciencedirect.com/science/article/pii/S1319157818304245 |
| work_keys_str_mv | AT oluwafolakeeojo formalverificationofapeertopeerstreamingprotocol AT ayodejiooluwatope formalverificationofapeertopeerstreamingprotocol AT surajuoajadi formalverificationofapeertopeerstreamingprotocol |