Proposed Algorithms to the State Explosion Problem
Model checking is a very powerful formal verification technique. Formal verification of complex systems is a major challenge in many areas of human society. The verification of properties of these systems is recognized as a difficult problem and faces a n
- PDF / 621,081 Bytes
- 7 Pages / 439.37 x 666.142 pts Page_size
- 77 Downloads / 193 Views
Faculty of Exact and Applied Sciences, Department of Computer Science, University of Oran 1 Ahmed Ben Bella, Oran, Algeria [email protected], [email protected] 2 Lab-STICC UMR CNRS 6285 ENSTA Bretagne, Brest, France {philippe.dhaussy,ciprian.teodorov}@ensta-bretagne.fr
Abstract. Model checking is a very powerful formal verification technique. Formal verification of complex systems is a major challenge in many areas of human society. The verification of properties of these systems is recognized as a difficult problem and faces a number of practical and theoretical problems. The main limitation of the formal verification is known as the state explosion problem. In this paper, we discuss about two contributions to this problem for the improvement of performance in time and memory space. Keywords: Model checking ration · Reachability graph
1
· State explosion problem · Parallel explo-
Introduction
Real time systems are often complex and critical, and require rigorous development to assert their functional and temporal correction. The technique called model checking is in this context, a very important tool for formal and automatic verification of a large class of systems. When the graph modeling the system is about reasonable size (it can be managed by the main memory), model checking methods are very effective in exploring this graph and detection of possible mistakes. However, most real software systems, have very large graphs size in a number of states. A state or a configuration, represents the behavior of a system at a moment. Indeed, the state space, represents all possible behaviors of a system. These important developments in graphs size known as the state explosion problem, is the main obstacle to the automatic verification by model checking. In this article, we cite two proposed solutions to this problem [2,3]. The first approach [2], is based on the concept of states compression in order to improve performances in memory space. The second solution [3], is based on a parallel exploration of state space, by distributing the state graph on several threads which allows a gain in execution time. Outline of the paper: the article is divided into 3 sections, the second section presents some works which offer solutions to the state explosion problem. Section 3 presents two solutions to the state explosion problem. c Springer Nature Singapore Pte Ltd. 2016 A. Unal et al. (Eds.): SmartCom 2016, CCIS 628, pp. 211–217, 2016. DOI: 10.1007/978-981-10-3433-6 26
212
2
L. Allal et al.
Related Work
Several studies have been performed to fight the state explosion problem [4,9,11]. In this section, we present some solutions to this problem. The approach proposed in [10], is based on a sequential algorithm. States are stored in their compressed form. The initial state is stored in an explicit way, the other states are stored in a compressed form. To verify if any generated state was explored, all states are decompressed which represents the disadvantage of this solution because the execution time can increase quickly. Viss
Data Loading...
