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 286
- Downloads 11
A model for evaluating performance of food industries supply chain management in Rasht Industriasl Town
Supply chain management, in 21st century, became important in improving organizations' ability to compete in the market and a significant progress is observed in this field. Supply chain management faces numerous challen...
The study of law of organization and administrative procedures of the court of justice in light of the principles of public law
Nowadays, due to the lack of laws and regulations, general principles of administrative courts have a double significance. These are unwritten rules, each of which could serve as guidelines for judges, government and cit...
A Study of the Effects of Globalization on Iranian Families
Globalization is a phenomenon that also has existed in the previous centuries. In the past, it had a very slow trend, but in the half of the recent century, because of the developments in mass media and widespread commun...
Implementation of knowledge managementin medium size company
This paper investigates the current knowledge management approaches and provides suggestions for a general improvement. Many researchers have worked with suggestions on how to improve the development process; software pr...
Study landslide Honam using GIS applications
The studied area is located in Crash- Zone of Zagros and known to Honam landslide.this landslide author that the mass separated from the limb northern Darikanan and moved to hillside .this area donot have regular slope r...