Model Checking

NuSmv (http://nusmv.fbk.eu/) is a symbolic model checker tool based of Model Checking theory. This latter, is a set of techniques to check the correctness of reactive systems like operation on database, operating systems tasks or any other job that require a continuous processing.

Model checking is an automatic technique that requires only the model of the task to check.  If the model is wrong, the model checker is able to return the counterexample in order to show which is the unexpected behaviour.

Let me show you an example: Shared / Exclusive Locking

The shared exclusive lock is a locking protocol used for serveral purpose like in DMBS item locking , or Kernel resources locking and so on. The purpose of this protocol is to make possible solely to read a resource when this resource is locked in read mode and avoid to read or write the resource if it is already locked in write mode.

This is the conflict matrix:

	Read	Write
Read	Y	N
Write	N	N

Below the NuSmv code:

MODULE main                                    
 VAR   
         
     rqueue_bool  : boolean;
      x_lock : {unlocked, write_locked, read_locked};
                                    
   t1 : process transaction(x_lock,rqueue_bool);             
   t2 : process transaction(x_lock,rqueue_bool);
  

    INIT x_lock=unlocked & rqueue_bool=FALSE;

---------------------------------------------------------------------
-----------------  CTL LANGUAGE ------------------------
---------------------------------------------------------------------

------ Conflict matrix for SHARED/EXCLUSIVE LOCK
------
------           _Read__Write_
------ Read  |___Y__|___N__|
------ Write  |___N__|__ N__|
------      

-- Impossible to W   when the itam is  W
SPEC  AG  !(t1.state =write_lock & t2.state =write_lock);   
SPEC  AG  !(t1.state =writing & t2.state =writing);   
    -- Impossible to W when the itam is R
SPEC  AG  !(t1.state =write_lock & t2.state =read_lock);   
SPEC  AG  !(t1.state =writing & t2.state =reading);   


-- Impossible R when the itam is W
SPEC  AG  !(t1.state =read_lock & t2.state =write_lock);   
SPEC  AG  !(t1.state =reading & t2.state =writing);


-- Possibile  to R when the item is R
SPEC  EF (t1.state =read_lock &  t2.state =read_lock);
-- counterexample
SPEC  AG !(t1.state =reading &  t2.state =reading);

 


MODULE transaction(x_lock,rqueue_bool)                         
 VAR                                           
   
   state   :{write_lock ,read_lock , wait, writing,reading};
 INIT             
      state = wait;
     
     
 ASSIGN 
 next (state) :=
  case

         -- if a transaction is waiting and item is not locked
         -- then the transaction can make read_lock/write_lock        
state = wait        & x_lock = unlocked                          : {read_lock,write_lock};
       
        -- if a transaction is waiting and the item is read locked 
        -- then the trasaction can only make  read_lock       
state = wait    & x_lock =read_locked                        : read_lock;
       
        -- if a transaction is in waiting and the item is locked in write mode then
        -- the transaction goes in wait
        state = wait    & x_lock =write_locked                    : wait;

        -- When a transaction is in read_lock then in the next state it must be in reading
        state = read_lock                                       : reading;

        -- When a transaction is in write_lock then in the next state it can go in reading or writing
        state = write_lock                                                        : {writing,reading};
        -- When a transaction is in reading o writing the in the next state it must be in wait
        state = writing | state = reading                             : wait;                
     
      TRUE :state;
  esac;
 
  next (x_lock) :=
  case
            -- If the next transaction state is read_lock then the item must be locked  in read mode 
            next(state) = read_lock   :read_locked;
            -- if the next transaction state is write_lock then the item must be locked in write mode
            next(state) = write_lock  :write_locked;
 
             -- if the transaction wrote/red the item then in the next state the transaction has to release the lock
            (state = writing | state = reading) &
            x_lock = write_locked & next(state) = wait  :unlocked;
             -- if the transaction wrote/read the item can release the lock only if no other transaction are locking it
            state = reading & x_lock = read_locked &  next(state) = wait & !rqueue_bool  :unlocked;
      TRUE :x_lock;
  esac;
 
  --- no_of_reads:
  next (rqueue_bool) :=
      case
            x_lock = read_locked & next(state)  = read_lock  :TRUE;
            x_lock = read_locked & next(state)  = wait  :FALSE;
              TRUE: rqueue_bool;
  esac;
 
 
FAIRNESS
    running