Case Studies in Symbolic Model Checking

Ganesh Gopalakrishnan, Dilip Khandekar, Ravi Kuramkote & Ratan Nalumasu

                            UUCS-94-009

                   Department of Computer Science
                        University of Utah
                     Salt Lake City, UT 84112

                           March 15, 1994


 
                              Abstract

Formal  verification of  hardware  and  software  systems has  long been 
recognized as an  essential step in the development process of a system.
It  is of  importance  especially in  concurrent  systems  that are more 
difficult to  debug than  sequential  systems.  Tools that are  powerful
enough to verify  real-life systems have become available recently.Model
checking  tools have become  quite popular  because of their  ability to
carry out  proofs with  minimal  human  intervention.  In this paper  we
report our experience with SMV, a symbolic model  verifier on  practical
problems of  significant sizes.  We present  verification of a  software
system, a  distributed shared memory  protocol,  and a  hardware system,
the  crossbar arbiter.  We discuss modeling of these  systems in SMV and 
their verification using  temporal logic  CTL queries.  We also describe
the problems encountered in tackling these examples and suggest possible
solutions.