(*) DISI Universita' di Genova
(**) UCSB University of California at Santa Barbara

• Introduction
• Tools
• Experimental results

Existing constraint technology like Presburger, and Boolean solvers, incorporated in the paradigm of symbolic model checking with rich assertional languages proposed by Kesten et al. at CAV 97 can be successfully applied to the verification of client-server protocols with arbitrary number of clients. Abstract interpretation is the mathematical bridge between protocol specification and constraint-based verification methods working on heterogeneous data like Tevfik Bultan's Action Language verifier of built on top of the Composite Symbolic Library. The method we propose is incomplete but fully automatic and sound for safety and liveness properties. The Action Language verified is, in fact, able to check full CTL temporal specifications. Sufficient conditions for the termination of the resulting verification algorithms can be derived using the general decidability results given by Abdulla et al.

The description of the approach is given in this tech-rep. 

The Action Language Verifier and the Composite Symbolic Library can be downloaded from here.

As a case-study, we apply the method to check safety and liveness properties for a formal model given through communicating finite-state machines of the directory-based consistency protocol proposed by Steven German.

The description of the protocol is given in the the tech-rep (the same as above).

The specification of the protocol using Action Language verifier is given below.

module main()
  enumerated state {Idle, ServeE, InvE, GrantE, ServeS, GrantS};
  boolean ex;
  integer xNull, xWaitS, xWaitE, xShared, xExclusive;
  initial: state=Idle && !ex && xNull>=1 && xShared=0 && xExclusive=0 &&
             xWaitE=0 && xWaitS=0;
  restrict: xNull>=0 && xWaitS>=0 && xWaitE>=0 && xShared>=0 &&
xExclusive>=0;

  module Request()
    reqS:    state=Idle && xNull>=1 &&
               state'=ServeS && xNull'=xNull-1 && xWaitS'=xWaitS+1;
    reqE1:   state=Idle && xNull>=1 &&
               state'=ServeE && xNull'=xNull-1 && xWaitE'=xWaitE+1;
    reqE2:   state=Idle && xShared>=1 &&
               state'=ServeE && xShared'=xShared-1 && xWaitE'=xWaitE+1;
    Request: reqS | reqE1 | reqE2;
  endmodule
                    
  module Serve()
    inv:     state=ServeS && ex && xExclusive>=1 &&
               state'=GrantS && xExclusive'=xExclusive-1 && xNull'=xNull+1
&& !ex;
    nonex:   state=ServeS && !ex &&
               state'=GrantS;
    invS:    state=ServeE &&
               state'=InvE && xNull'=xNull+xShared && xShared'=0;
    invE:    state=InvE && ex && xExclusive >=1 &&
               state'=GrantE && xNull'=xNull+1 && xExclusive'=xExclusive-1
&& !ex;
    nonexE:  state=InvE && !ex &&
               state'=GrantE;
    Serve :  inv | nonex | invS | invE | nonexE;
  endmodule
                                      
  module Grant()
    grantS:   state=GrantS && xWaitS>=1 &&
                state'= Idle && xWaitS'=xWaitS-1 && xShared'=xShared+1;
    grantE:   state=GrantE && xWaitE>=1 &&
                state'=Idle && xWaitE'=xWaitE-1 &&
xExclusive'=xExclusive+1 && ex';
    Grant :   grantS | grantE;
  endmodule

  main: Request() | Serve() | Grant();
  spec: AG([!((xShared>=1 && xExclusive>=1) || xExclusive>=2)])
endmodule

machine refined_protocol 
number_of_nodes 10
number_of_dynamic_variables 5
number_of_transitions 14
initial_node 0
static_variables
variable_ranges
{[xN,xWS,xWE,xS,xE] : xN,xWS,xWE,xS,xE >= 0} 
initial_condition
{[xN,xWS,xWE,xS,xE] : xN>=1 && xS=0 && xE=0 && xWE=0 && xWS=0}
transition_list


##### Request

# transition reqS  (ex=ex'=false)
        source_node 0
        destination_node  2
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS',xWE,xS,xE] : 
 xN>=1 && xN'=xN-1 && xWS'=xWS+1
}

# transition reqS  (ex=ex'=true)
        source_node 1
        destination_node  3
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS',xWE,xS,xE] : 
 xN>=1 && xN'=xN-1 && xWS'=xWS+1
}


# transition reqE1  (ex=ex'=false)
        source_node 0
        destination_node 4 
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS,xWE',xS,xE] : 
 xN>=1 && xN'=xN-1 && xWE'=xWE+1
}

# transition reqE1  (ex=ex'=true)
        source_node 1
        destination_node 5
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS,xWE',xS,xE] :
 xN>=1 && xN'=xN-1 && xWE'=xWE+1
}

# transition reqE2  (ex=ex'=false)
        source_node 0
        destination_node 4
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE',xS',xE] : 
 xS>=1 && xS'=xS-1 && xWE'=xWE+1
}

# transition reqE2  (ex=ex'=true)
        source_node 1
        destination_node 5
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE',xS',xE] : 
 xS>=1 && xS'=xS-1 && xWE'=xWE+1
}


##### Serve 

# transition inv1  (ex=ex'=true)
        source_node 3
        destination_node 3
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS,xWE,xS',xE] :
  xS>=1 && xS'=xS-1 && xN'=xN+1
}

# transition inv1  (ex=ex'=false)
        source_node 2
        destination_node 2
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS,xWE,xS',xE] :
  xS>=1 && xS'=xS-1 && xN'=xN+1
}

# transition inv1  (ex=true & ex'=false)
        source_node 3
        destination_node 2 
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN',xWS,xWE,xS,xE'] : 
  xE>=1 && xE'=xE-1 && xN'=xN+1
}


# transition nonex  (ex=ex'=false)
        source_node 2
        destination_node 6
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE,xS,xE] }


# transition inv2  (ex=ex'=false)
        source_node 4
        destination_node 8
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE,xS,xE] : 
  xS=0 && xE=0 
}

# transition inv2  (ex=ex'=true)
        source_node 5
        destination_node 9
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE,xS,xE] : 
  xS=0 && xE=0
}


##### Grant

# transition grantS  (ex=ex'=false)
        source_node 6
        destination_node 0
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS',xWE,xS',xE] : 
  xWS>=1 && xWS'=xWS-1 && xS'=xS+1
}

# transition grantS  (ex=ex'=true)
        source_node 7
        destination_node 1
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS',xWE,xS',xE] : 
  xWS>=1 && xWS'=xWS-1 && xS'=xS+1
}

# transition grantE  (ex=false & ex'=true)
        source_node 8
        destination_node 1
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE',xS,xE'] : 
  xWE>=1 && xWE'=xWE-1 && xE'=xE+1 
}

# transition grantE  (ex=ex'=true)
        source_node 9
        destination_node 1
        transformation_relation
{[xN,xWS,xWE,xS,xE] -> [xN,xWS,xWE',xS,xE'] : 
  xWE>=1 && xWE'=xWE-1 && xE'=xE+1 
}


formula_list

AG( {[xN,xWS,xWE,xS,xE] : !(xS>=1 && xE>=1 || xE>=2) } )

# AG( {[xN,xWS,xWE,xS,xE] : xE >= 0} )

# AG({[xN,xWS,xWE,xS,xE] : xWS>=1} => EF({[xN,xWS,xWE,xS,xE] : xS>=1}))

# AG({[xN,xWS,xWE,xS,xE] : xWS>=1} => AF({[xN,xWS,xWE,xS,xE] : xS>=1}))

# AG({[xN,xWS,xWE,xS,xE] : xWS>=2} => EF({[xN,xWS,xWE,xS,xE] : xS>=2}))

# AG({[xN,xWS,xWE,xS,xE] : xWS>=2} => AF({[xN,xWS,xWE,xS,xE] : xS>=2}))

# AG({[xN,xWS,xWE,xS,xE] : xWE>=1} => EF({[xN,xWS,xWE,xS,xE] : xE>=1}))

# AG({[xN,xWS,xWE,xS,xE] : xWE>=1} => AF({[xN,xWS,xWE,xS,xE] : xE>=1}))

end