Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Distributed algorithm to fight the state explosion problem

Lamia Allal 1 Ghalem Belalem 1 Philippe Dhaussy 2 Ciprian Teodorov 2
2 Lab-STICC_ENSTAB_ CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
Abstract : Model checking, introduced 20 years ago, combines several fully automatic techniques in which the property to be checked is tested exhaustively on all the possible executions of the system. It is an automated approach to verifying that a system meets its specifications. The main limit to the use of model checking is related to the state explosion problem, which occurs when the number of states increases exponentially according to the complexity of the system. In this article, we presented a distributed exploration algorithm executed on two different architectures to fight this problem. The first one is using two real machines interconnected across the network and the second using two virtual machines in a cloud computing. We carried out a comparative study between these two distributed approaches as well as a parallel algorithm. The aim of this paper is to give the advantages and drawbacks of each solution.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-01716143
Contributeur : Ciprian Teodorov <>
Soumis le : vendredi 23 février 2018 - 13:26:10
Dernière modification le : mercredi 24 juin 2020 - 16:19:51

Identifiants

Citation

Lamia Allal, Ghalem Belalem, Philippe Dhaussy, Ciprian Teodorov. Distributed algorithm to fight the state explosion problem. INDERSCIENCE International Journal of Internet Technology and Secured Transactions., Inderscience Enterprises, 2018, 8 (3), pp.398 - 411. ⟨10.1504/IJITST.2018.10014833⟩. ⟨hal-01716143⟩

Partager

Métriques

Consultations de la notice

439