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 315
- Downloads 11
history of Elegy writing in Arabic literature, Islamic era
Requiem for chorus burner, moaning is a lost man in the Parting of Friends of the oldest and most honest human Poems counts. It can be said that human language is the most honest , because it is most closely connected wi...
The relations between Job Satisfaction dimensions with Organizational Commitment of personnel
The general goal of this plan is finding any relations among different dimensions of job satisfaction and organizational commitment of personnel at saman cement company. Specific goals of this project are follows: Recogn...
Investigation of the efficiency of UV/H 2 O 2 process on the removal of Rhodamine B from aqueous solutions
Background: Textile wastewater contains toxic and hard biodegradable materials, which discharge of them into environment specially receiving water, have irreparable effects. Methods: In the present study the combination...
The effect of microelements spraying on growth, qualitative and quantitative grain corn in Iran
Most of the soils of Iran are calcareous and micro nutrient deficiency is a usual problem in such soils. Then, this study was conducted in research site of Islamic Azad University-Isfahan branch to evaluate effects of fo...
Elders Fall Risk Predictors
The matter of falling plays an important role in the quality of older peoples’ life for which lots of tools that single vulnerable elders out. This study is to recognize and introduce these tools. Using key words regardi...