Đang chuẩn bị liên kết để tải về tài liệu:
Parallelizing random-walk based model checking

In model checking, a formal methods technique to verify a system with some desired properties, the guidance techniques have been employed a long time ago in driving the verification into area of error in the state space. Another technique is to choose the next state to be explored in a walk randomly to avoid the wrong guidance. | SCIENCE & TECHNOLOGY DEVELOPMENT, Vol.18, No.K5 - 2015 Parallelizing random-walk based model checking Thang H. Bui Ho Chi Minh city University of Technology - Vietnam National University Ho Chi Minh City, Vietnam (Manuscript Received on May 18nd, 2014, Manuscript Revised August 28nd, 2015) ABSTRACT In model checking, a formal methods technique to verify a system with some desired properties, the guidance techniques have been employed a long time ago in driving the verification into area of `error` in the state space. Another technique is to choose the next state to be explored in a walk randomly to avoid the `wrong` guidance. When the latter is a nonexhaustive technique in the sense that only a manageable number of walks are carried out before the search is terminated, it does scale well. In enhancing the technique to use recently powerful parallel/multi-core systems, research on parallelizing the algorithm shall be carried out. In this work, we propose a method that parallelizes the random-walk algorithm. It also increases the completeness of the non-exhaustive algorithm. The experimentation has shown the great improvement of the proposed algorithm compares to the original once. Keywords: Model checking, random-walk, parallelization, multi-core. 1. INTRODUCTION When software and hardware nowadays are used widely in society and human life, their correctness is the most challenge in system designing and implementing. Therefore, model checking, a formal methods approach, that verifies a given system with a desired property, is used recently in guarantee the correctness of the system. Traditionally, it is an exhaustive search on the state space of a system to ensure that no state violates the given property. Unfortunately, it faces the `state space TRANG 108 explosion` problem in searching the state space. Although the use of heuristic guidance can improve the performance, model checking in reality is said not to scale well. Random-walk search, that draws .