Model Checking Based on Simultaneous Reachability Analysis

13 years 9 months ago
Model Checking Based on Simultaneous Reachability Analysis
Abstract. Simultaneous reachability analysis SRA is a recently proposed approach to alleviating the state space explosion problem in reachability analysis of concurrent systems. The concept of SRA is to allow a global transition in a reachability graph to contain a set of transitions of di erent processes such that the state reached by the global transition is independent of the execution order of the associated process transitions. In this paper, we describe how to apply the SRA approach to concurrent systems for model checking. We rst describe an SRA-based framework for producing a reduced state graph that provides su cient information for model checking. Following this framework, we present an algorithm that generates a reduced state graph for the extended nite state machine EFSM model with multiple ports. Empirical results indicate that, our SRA reduction algorithm performs as good as or better than the partial order reduction algorithm in SPIN.
Bengi Karaçali, Kuo-Chung Tai
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where SPIN
Authors Bengi Karaçali, Kuo-Chung Tai
Comments (0)