https://hal.inria.fr/inria-00423583Lang, FrédéricFrédéricLangVASY - System validation - Research and applications - Inria Grenoble - Rhône-Alpes - Inria - Institut National de Recherche en Informatique et en Automatique - LIG - Laboratoire d'Informatique de Grenoble - UPMF - Université Pierre Mendès France - Grenoble 2 - UJF - Université Joseph Fourier - Grenoble 1 - Grenoble INP - Institut polytechnique de Grenoble - Grenoble Institute of Technology - INPG - Institut National Polytechnique de Grenoble - CNRS - Centre National de la Recherche ScientifiqueMateescu, RaduRaduMateescuVASY - System validation - Research and applications - Inria Grenoble - Rhône-Alpes - Inria - Institut National de Recherche en Informatique et en Automatique - LIG - Laboratoire d'Informatique de Grenoble - UPMF - Université Pierre Mendès France - Grenoble 2 - UJF - Université Joseph Fourier - Grenoble 1 - Grenoble INP - Institut polytechnique de Grenoble - Grenoble Institute of Technology - INPG - Institut National Polytechnique de Grenoble - CNRS - Centre National de la Recherche ScientifiquePartial Order Reductions using Compositional Confluence DetectionHAL CCSD2009[INFO.INFO-MO] Computer Science [cs]/Modeling and SimulationMckinty, Christine2009-10-12 10:26:082022-07-06 04:17:272009-10-12 11:54:23enConference papersapplication/pdf1Explicit state methods have proven useful in verifying safety critical systems containing concurrent processes that run asynchronously and communicate. Such methods consist of inspecting the states and transitions of a graph representation of the system. Their main limitation is state explosion, which happens when the graph is too large to be stored in the available computer memory. Several techniques can be used to palliate state explosion, such as on-the-fly verification, compositional verification, and partial order reductions. In this paper, we propose a new technique of partial order reductions based on compositional confluence detection (Ccd), which can be combined with the techniques mentioned above. Ccd is based upon a generalization of the notion of confluence defined by Milner and exploits the fact that synchronizing transitions hat are confluent in the individual processes yield a confluent transition in the system graph. It thus consists of analysing the transitions of the individual process graphs and the synchronization structure to identify such confluent transitions compositionally. Under some additional conditions, the confluent transitions can be given priority over the other transitions, thus enabling graph reductions. We propose two such additional conditions: one ensuring that the generated graph is equivalent to the original system graph modulo branching bisimulation, and one ensuring that the generated graph contains the same deadlock states as the original system graph. We also describe how Ccd-based reductions were implemented in the Cadp toolbox, and present examples and case study in which adding Ccd improves reductions with respect to compositional verification and other partial order reductions.