Partial Order Reductions Using Compositional Confluence Detection

Abstract. Explicit state methods have proven useful in verifying safetycritical 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 that are confluent in the individual processes yield a confluent transition in the system graph. It thus consists of analysing the transitio...

• Type: Journal
• Year: 2009
• Where: FM
• Authors: Frédéric Lang, Radu Mateescu
• Keywords: Compositional Verification, Confluent Transitions, FM 2009, Formal Methods, Partial Order Reductions