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 320
- Downloads 11
Myth and its historical roots in Iran and the world
This study aimed to investigate and Myths of the world are explained. The tale is a story with many different themes and concepts, and sometimes incorporate Ghyrhqyqy imagination and events around the world with a long h...
Prevalence of Neurological Complications Caused by Shigellosis in Children Hospitalized at Qom Children Hospital
This descriptive cross-sectional study attempted to determine the prevalence of neurological complications caused by shigellosis at Qom Children Hospital.The study was conducted March 2010 to June 2012 on 1 month to 12-y...
Use of ethanol, methanol and essential oils to improve vase-life of chrysanthemum cut flowers
The production of chrysanthemum cut flowers has been rapidly increasing in the world. However, a relatively limited vase life reduces its marketability. An experiment was conducted to research the effect of different con...
Metadiscourse in Essay Writing: An EFL Case
The purpose of this study was to investigate whether discourse markers training leads to a better writing performance of the EFL learners. The participants of this study were 32 male Iranian students majoring in Mechanic...
The correlation between nesfatin-1 and blood pressure in healthy normal weight and obese adults
Nesfatin-1 is an anorexigenic peptide with 82 aminoacides expresses in hypothalamic cells, adipose tissue, gastric mucous and pancreatic ?-cells. Its precursor protein is named nucleobindin-2 (NUCB2). Recently it is sugg...