GUESSING, MODEL CHECKING AND THEOREM PROVING OF STATE MACHINE PROPERTIES – A CASE STUDY ON QLOCK

GUESSING, MODEL CHECKING AND THEOREM PROVING OF STATE MACHINE PROPERTIES – A CASE STUDY ON QLOCK

May Thu Aung1, Tam Thi Thanh Nguyen2, Kazuhiro Ogata2

1Faculty of Information Science,
University of Information Technology, Parami Road, Hlaing Campus, Yangon, Myanmar.
2School of Information Science,Japan Advanced Institute of Science and Technology,
1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan.

ABSTRACT
It is worth understanding state machines better because various kinds of systems can be formalized as state machines and therefore understanding state machines has something to do with comprehension of systems. Understanding state machines can be interpreted as knowing properties they enjoy and comprehension of systems is interpreted as knowing whether they satisfy requirements. We (mainly the second author) have developed a tool called SMGA that basically takes a finite sequence of states from a state machine and generates a graphical animation of the finite sequence or the state machine. Observing such a graphical animation helps us guess properties of the state machine. We should confirm whether the state machine enjoys the guessed properties because such guessed properties may not be true properties of the state machine. Model checking is one possible technique to do so. If the state machine has a fixed small number of reachable states, model checking is enough. Otherwise, however, it is not. If that is the case, we should use some other techniques to make sure that the system enjoys the guessed properties. Interactive theorem proving is one such technique. The paper reports on a case study in which a mutual exclusion protocol called Qlock is used as an example to exemplify the abovementioned idea or methodology.


Keywords: graphical animations of state machines, model checking, theorem proving, invariant properties

pdf ico FULL PAPER


 
 
 
 
 

Contact Us

Managing Editor of IJSECS
Faculty of Computer Systems & Software Engineering (FSKKP)

Universiti Malaysia Pahang
Lebuhraya Tun Razak
26300 Gambang,
Kuantan, Pahang Darul Makmur.

Tel: +609 549 2133
Fax: +609 549 2144
Email: ijsecsfskkp@ump.edu.my

Visitor Counter

0057472
Today
Yesterday
This Week
Last Week
This Month
Last Month
All days
83
131
573
588
1803
2435
57472