A Survey on Coping with the State Space Explosion Problem in Model Checking
Journal Title: International Research Journal of Applied and Basic Sciences - Year 2013, Vol 4, Issue 6
Abstract
Today, computer systems play a significant role in our daily lives. They are used in many different fields such as: smart cards, mobile phones, smart devices, telecommunication systems, ecommerce, banking system and etc. However, the more computer systems penetrate our lives, the more complicated they get. On the other hand, some of them are used in critical applications in which a bug or an error can be fatal, catastrophic and causes a huge loss of money, like: nuclear plants, chemical plants, aviation systems, biological devices and etc. Therefore, this kind of computer systems needs more accurate and precise type of verification than the traditional test and simulation techniques. Hence, formal software verification approaches use instead. Model checking is an effective and efficient type of formal verification which has been used for verification of safety-critical systems in last two decades. In model checking technique, the system which has to be verified, is modeled as a finite state machine in which nodes are system states and edges are transitions between those states. The major drawback of model checking approach is state space explosion which means the number of states needed to model the system exceeded the amount of available memory. There are several methods to fight the state space explosion. This survey provides a perspective on these techniques and reviews some of the previous articles.
Authors and Affiliations
Vahid Rafe| Department of Computer Engineering, Faculty of Engineering, Arak University, Arak 38156-8-8349, Iran, v-rafe@araku.ac.ir, Mohsen Rahmani| Department of Computer Engineering, Faculty of Engineering, Arak University, Arak 38156-8-8349, Iran, Kianoosh Rashidi| Department of Computer Engineering, Faculty of Engineering, Arak University, Arak 38156-8-8349, Iran
Keywords
Related Articles
- EP ID EP5474
- DOI -
- Views 326
- Downloads 11
Evaluation the affecting factors on the leadership style of managers in the Agricultural jihad in Guilan province
Since the leadership style of managers consist of affection factors in creativity, motivation, vocational satisfaction and staffs efficiency. Identification and evaluating the affecting factors on leadership style of man...
Supplication in Atar’s Mantegoteir book
Theosophy and its learning is one of the solutions in reach to holy god. In this case tears and sadness, supplication is primarily and preliminary for behavior and traverse toward theosophy. Atar Nyshapvry is one of this...
Study on the effect of cutting location on shoot and IBA on rooting of ‘Night Jessamine’ (Cestrum nocturnum) stem cuttings
In order to evaluate of the cutting location on shoot and Indule butyric acid (IBA) on rooting of ‘Night Jessamine’ (Cestrum nocturnum) stem cuttings, this study was performed as factorial arrangement in randomized compl...
Principles of disinfecting domestic wastewater for irrigation
In order to remove pathogens from wastewater to be used in agriculture, World Health Organization (WHO) has published a guide book titled “Guidelines for the safe use of wastewater excreta and gray water” in four volumes...
The effect of 12 weeks Circuit-resistance training on Cortisol, Body Composition and Muscular Strength in overweight young males
Resistance exercise has increasingly become a mode of exercise recommended for weight management and weight loss in obese individuals. Cortisol is an effective catabolic hormone in metabolism. The purpose of this study w...