[SAL] Using recursive datatypes with model checker

mwwhalen at rockwellcollins.com mwwhalen at rockwellcollins.com
Tue Apr 17 11:49:46 PDT 2007


Hello all,

  Is it possible to use recursive types (e.g., list) defined as DATATYPEs
with the SAL model checking tools?  I tried creating a list datatype and
defining a couple of operations, but got errors of various sorts from the
different model checking tools (sal-smc, sal-inf-bmc) related to
finiteness.  Here's my small example:

listtest: CONTEXT =
BEGIN
   id: TYPE ;

   id_list : TYPE =
      DATATYPE
         nil,
         node(hd: id, tl: id_list)
      END  ;

   IDL : id_list ;

   length: [id_list -> NATURAL] =
      LAMBDA (lst: id_list):
         IF nil?(lst) THEN 0 ELSE 1 + length(tl(lst)) ENDIF ;

   system : MODULE =
   BEGIN
      OUTPUT out_L : id_list
   DEFINITION
      out_L = IDL ;
   END ;

   prop: THEOREM system |- G(length(out_L) < 5);

END

Obviously, I'm not constraining IDL so there are essentially an infinite
number of constants to check.  Are there any constraints that I can place
on the use of recursive datatypes (e.g., max size) in order to meet
finiteness constraints in SAL?  Anyone else tried to use recursive
datatypes and have any models lying around?

Thanks for your time!

:-) Mike

--------------------------------------
Dr. Michael Whalen
Rockwell Collins Inc.
7805 Telegraph Rd. Suite 100
Bloomington, MN 55438

RCI Office Phone: 319-263-2568
UMN Office Phone: 612-625-4543
Cell Phone: 651-442-8834



More information about the SAL mailing list