Using Parallel and Distributed Reachability in Model Checking

Lamia Allal (1) , Ghalem Belalem (1) , Philippe Dhaussy (2) , Ciprian Teodorov (2)

1 University of Oran
2 Lab-STICC_ENSTAB_ CACS_MOCS

In the life cycle of any software system, a crucial phase of formalization and validation by means of verification and/or testing leads to the identification of probable errors infiltrated during its design. Model checking is one of the formal verification techniques. This technique is very powerful, but limited by the state explosion problem that occurs when the model to be checked is too large, and cannot be verified for lack of memory space. In this article, we cite two solutions, parallel and distributed, which aim to reduce the state space explosion. A comparative study between these approaches is carried out on a counters model.

Mots clés: Formal verification; Distributed exploration; Parallel exploration; Model checking; State explosion problem

Domaines: Informatique [cs]; Génie logiciel [cs.SE]

Lamia Allal, Ghalem Belalem, Philippe Dhaussy, Ciprian Teodorov. Using Parallel and Distributed Reachability in Model Checking. Recent Advancement in Computer, Communication and Computational Sciences (RACCCS-2017), Sep 2017, Ajmer, India. pp.143-154, ⟨10.1007/978-981-10-7386-1_12⟩. ⟨hal-01780556⟩