Title: Distributed algorithm to fight the state explosion problem

Authors: Lamia Allal; Ghalem Belalem; Philippe Dhaussy; Ciprian Teodorov

Addresses: Laboratory of Computer Science of Oran, Department of Computer Science, University of Oran 1, Ahmed Ben Bella, Algeria ' Laboratory of Computer Science of Oran, Department of Computer Science, University of Oran 1, Ahmed Ben Bella, Algeria ' UEB, Lab-STICC Laboratory UMR CNRS, 6285, ENSTA Bretagne, Brest, 29806, France ' UEB, Lab-STICC Laboratory UMR CNRS, 6285, ENSTA Bretagne, Brest, 29806, France

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.

Keywords: model checking; state explosion problem; parallel exploration; distributed exploration; execution time; memory space.

DOI: 10.1504/IJITST.2018.093664

International Journal of Internet Technology and Secured Transactions, 2018 Vol.8 No.3, pp.398 - 411

Received: 01 Mar 2017
Accepted: 28 Apr 2017

Published online: 31 Jul 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article