Local Verification Using a Distributed State Space

Article type: Research Article

Authors: Abid, Chiheb Ameur | Zouari, Belhassen

Affiliations: LIP2 Laboratory, University of Tunis - El Manar 2092, Tunis, Tunisia. chiheb.abid@gmail.com; belhassen.zouari@fst.rnu.tn

Note: [] Address for correspondence: LIP2 Laboratory - University of Tunis - El Manar 2092, Tunis, Tunisia

Abstract: This paper deals with the modular analysis of distributed concurrent systems modelled by Petri nets. The main analysis techniques of such systems suffer from the well-known problem of the combinatory explosion of state space. In order to cope with this problem, we use a modular representation of the state space instead of the ordinary one. The modular representation, namely modular state space, is much smaller than the ordinary state space. We propose to distribute the modular state space on every machine associated with one module. We enhance the modularity of the verification of some local properties of any module by limiting it to the exploration of local and some global information. Once the construction of the distributed state space is performed, there is no communication between modules during the verification.

Keywords: Distributed systems, modular verification, Petri nets, state space explosion

DOI: 10.3233/FI-2013-850

Journal: Fundamenta Informaticae, vol. 125, no. 1, pp. 1-20, 2013