Change search
ReferencesLink to record
Permanent link

Direct link
Verification of P2P live streaming systems using symmetry-based semiautomatic abstractions
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-6468-1605
Universidade Federal de Minas Gerais.
Universidade Federal de Juiz de Fora.
2012 (English)In: Proceedings of the 2012 International Conference on High Performance Computing and Simulation, HPCS 2012, IEEE , 2012, 343-349 p.Conference paper (Refereed)
Abstract [en]

P2P systems are one of the most efficient data transport technologies in use today. Particularly, P2P live streaming systems have been growing in popularity recently. However, analyzing such systems is difficult. Developers are not able to realize a complete test due the due to system size and complex dynamic behavior. This may lead us to develop protocols with errors, unfair or even with low performance. One way of performing such an analysis is using formal methods. Model Checking is one such method that can be used for the formal verification of P2P systems. However it suffers from the combinatory explosion of states. The problem can be minimized with techniques such as abstraction and symmetry reduction. This work combines both techniques to produce reduced models that can be verified in feasible time. We present a methodology to generate abstract models of reactive systems semi-automatically, based on the model's symmetry. It defines modeling premises to make the abstraction procedure semiautomatic, i.e., without modification of the model. Moreover, it presents abstraction patterns based on the system symmetry and shows which properties are consistent with each pattern. The reductions obtained by the methodology were significant. In our test case of a P2P network, it has enabled the verification of liveness properties over the abstract models which did not finish with the original model after more than two weeks of intensive computation. Our results indicate that the use of model checking for the verification of P2P systems is feasible, and that our modeling methodology can increase the efficiency of the verification algorithms enough to enable the analysis of real complex P2P live streaming systems.

Place, publisher, year, edition, pages
IEEE , 2012. 343-349 p.
Keyword [en]
Formal Verification, Model Checking, Symmetry, Abstraction, Under-approximation, P2P Live Streaming
National Category
Computer Systems
Research subject
SRA - E-Science (SeRC)
URN: urn:nbn:se:kth:diva-104237DOI: 10.1109/HPCSim.2012.6266935ScopusID: 2-s2.0-84867001711ISBN: 978-1-4673-2359-8OAI: diva2:563619
10th Annual International Conference on High Performance Computing and Simulation, HPCS 2012; Madrid; 2 July 2012 through 6 July 2012
Swedish e‐Science Research Center

QC 20121122

Available from: 2012-10-30 Created: 2012-10-30 Last updated: 2012-11-22Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
de Carvalho Gomes, Pedro
By organisation
Theoretical Computer Science, TCS
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 28 hits
ReferencesLink to record
Permanent link

Direct link