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 287
- Downloads 11
gap engineering in two-dimensional photonic quasicrystal with twelvefold symmetry
Photonic quasicrystals are special class of aperiodic crystals , which can exhibit photonic band gaps, But the lack of periodicity in the quasiperiodic structures make impossible the determining a unitcell for the calcul...
The effect of the Slow-Stroke back massage on fatigue of dialyzed patients
Fatigue is the most common side effect that is known as one of the most stressful factors, and it is expressed as a debilitating factor, aim of this study was to study the effect of back massage on fatigue in hemodialysi...
The relationship between the competitive-trait anxiety and the rate of sports injuries in professional soccer players
Soccer as well as many other sports requires high levels of psychological skills. However, previous studies only examined the association between psychological factors as a whole (general) deal with sports injuries and i...
Relationship between Alexithymia, Body mass index and Eating irrational beliefs in Teens
This study examined the relationship between alexithymia , body mass index and eating disorders beliefs in teenagers. The staticalsample this research were 209 high school females who selected by random cluster sampling...
Examining the Effect of Official Automation on Improvement of Mangers’ Decision Making (Case Study: Bokan Saderat Bank)
The aim of the present study is to examine the effect of official automation on improvement of mangers’ decision making. The study is applied, descriptive and survey in terms of goal, quality of data collection and quali...