• Chỉ mục bởi
  • Năm xuất bản

Using multi decision diagram in model checking

Khanh N.T. School of Computing, National University of Singapore, Singapore|
Tho Q.T. Faculty of Computer Science and Engineering, Hochiminh City University of Technology, Viet Nam|

SSIRI-C 2010 - 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion Số , năm 2010 (Tập , trang 126-129)

DOI: 10.1109/SSIRI-C.2010.31

Tài liệu thuộc danh mục: Scopus

Conference Paper


Từ khóa: Automatic verification; Complex systems; Concurrent systems; Decision diagram; Explicit model checking; Hash table; Memory efficient; Memory resources; Model checker; Multi decision diagram; Number of state; State space; State-space explosion; System state; Software reliability; Model checking
Tóm tắt tiếng anh
Model checking[1] is an automatic verification technique for finite concurrent systems. In this method, the assertion is verified by exhaustively searching over the state space. However, the number of states of the system will grow exponentially with the number of processes. It limits model checker to handle with complex systems. In explicit model checking[1], system states are explored one-by-one and stored in memory explicitly, so the verified system is restricted by the memory resource. Most of the memory is consumed by the hash table which contains the visited states and the queue of states whose successors are already generated. In this paper, we will present a new way of storing the visited states by using a tree. We show that our approach is memory efficient. Organization of the report: Section 1 is the introduction, and section 2 introduces PAT model checker. Section 3 describes how to implement the tree storing the visited states. Section 4 presents the heuristic to improve the performance for the tree. Section 5 is the experiment result. Lastly section 6 is the conclusion and future work. � 2010 IEEE.

Xem chi tiết