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 325
- Downloads 11
genetic principles and persuasive methods of quran
Quran is the human's life charter that includes three attributes of worldly, eternity, and universality. So it should be based on irrepealable, knowledgeable, and commitment principles. Only that knowledge is irrepealabl...
Effect of different levels of energy and protein with constant ratio on performance and carcass characteristics in broiler chickens
The aim of this study was to determine the effect of different levels of energy and protein with constant ratio on performance and carcass characteristics in broiler chickens. Three experimental diets were formulated to...
The Impact of Brand Extension on New Product from Customers’ Perspective
Today, most manufacturers distribute their new products under the brands of previous successful products since one of the most valuable properties of each organization is its background and how it is perceived as a reput...
A Survey on the Nature Human Trafficking Based on criminal law in Iran
Today human trafficking has taken a new catastrophic form and thousands of victims are being smuggled each year. In spite of the vast increase in this crime on international level, there is a very low level of academic w...
Study of the relationship between knowledge management and organizational culture Case study: agriculture organization of Qom
The present research with the topic of, the study of the relationship between knowledge management and organizational culture of Qom province’s social security administration is presented. The aim of this study is to dis...