SPIN NEWS - Nr. 6 - June 5, 1995

Contents of this NewsLetter:

Recent Extensions to SPIN

There have been six updates of the Spin and Xspin sources since the last Newsletter. (The current version is 2.4.1) A couple of the more interesting extensions are:

  1. Breakpointing in Xspin Simulations

    You can now set breakpoints in a model, which will suspend a running simulation in XSPIN when it is encountered. Breakpoints are kept invisible from SPIN itself by hiding the syntax into printf statements. It was already true that any printf statement of the following type would be made visible in XSPIN graphical Message Sequence Charts (MSC)

    	printf("MSC: ....anything...\n", parameters)
    
    To set a breakpoint, use:
    	printf("MSC: BREAK ... anything else\n")
    
    Breakpoints can be made conditional by using regular PROMELA semantics.

  2. Quickstart for long Error.trails

    If you do large-scale applications of SPIN, you can often get pretty lengthy error trails, that can take Xspin a while to traverse with a guided simulation. You can try to generate shorted versions of an error trail, by restricting the search depth (and repeating the verification run) until you iteratively discover the smallest search depth that still produces an error trail, but that is not always convenient to do.

    In most cases, merely looking at the last 20 or 30 steps in the error trail can reveal the cause of the error sufficiently clearly that it can be fixed. Spin and Xspin therefore now support an option to skip over the first N steps of an error trail, when following error trails (i.e., in guided simulations). (Th first part of the trail is still traversed in the background of course, but it will be invisible and very fast.) Xspin simply has an extra entry-widget in the display for using this feature. Spin supports a new option -jN to do the same, where N is the number of steps to skip.
    Example:

    	spin -t -p -j1000 spec  # skip initial 1000 steps
    
    (the trail better be longer than 1000 steps of course...)

  3. Dumping Multiple Error.trails

    The verifiers produced by SPIN produce a single error trail by default. Runtime option -cN can be used to select the Nth error that is encountered in the depth-first search, but still only one error trail is written into the file system. There is a new runtime option now, -e, that tells the verifier to write out *every* error trail it encounters - up to the limit set by -cN, as before (N is still 1 by default). This is expected to be useful especially when SPIN is used for test-sequence generation (with the help of never-claims; more about this will follow in later newsletters).
    Example:

    	pan -e -c5    # generate first 5 complete trails
    
  4. Single-Bit Hashing, Changing Hash Functions

    There has been new interest in expanding the use of the bitstate hashing techniques. To allow any SPIN user to reproduce some of the experiments that have appeared in the recent literature, there are now two additional runtime options:

    	-hN	selects one of 32 different independent hash
    		functions (the default behavior is -h0)
    	-s	selects single bithashing, instead of the
    		default double bithashing scheme
    	-RN	repeats a verification automatically up to
    		N times, each time with a different hash
    		function.
    		N can be any number 1..32 (default is -R1).
    
    Examples (assuming compilation for Bitstate search):
    	pan -h12    # doublebit hashing, with 12th function
    	pan -s      # singlebit hashing, default hash
    	pan -s -h5
    	pan -s -R32 # 32 sequential singlebit runs
    	pan -R32    # idem, but with doublebit hashing
    
  5. Compatibility of Xspin with Tcl7.4/Tk4.0

    The Xspin sources were modified to make the compatible with the new distribution of Tcl7.4/Tk4.0, which is now installed as a beta test on many systems. There is no change in behavior. Starting with version 2.4.1, there is also a separate upgrades script for the Xspin sources (by popular demand), to help you avoid having to repeat the customization process each time you renew the Xspin sources. Be careful, though, if you make changes in the sources manually as well: don't change the line number on which existing code sits, or the upgrade scripts will fail to make the proper incremental changes later.

The Subscribe Option of Netlib

If you email a oneline message:

	mail netlib.bell-labs.com
	subscribe spin
	.
you will automatically receive reminders from the netlib demon whenever one of the files in the /netlib/spin distribution is changed. Use with caution: this may be more information than you need. The newsletters will keep you up to date of major changes, so this is probably only needed if you want to follow the updates more closely than that.

This is independent from the distribution of these newsletters. To subscribe to the newsletter, send the oneline message:

	mail [email protected]
	subscribe to spin list
	.

A New SPIN Documents Database

There is a tentative plan to build a shared repository of papers, reports, memoranda, project descriptions, etc. of both theoretical and practical work that relates to the SPIN system in some way, or that may be of interest in general to verification people. This would include both published and (especially) unpublished papers and reports. The plan is to store all documents in postscript form, and make them accessible on the world wide web.

For papers that cannot be made available via ftp or Mosaic/Netscape (perhaps for copyright reasons), the database can maintain an up to date Bibliography where publications are listed.

The database can also include position statements, papers, etc, submitted for the upcoming SPIN workshop in Montreal in October.

Nothing much has been decided at this point -- not even where or by whom this database will be maintained and administered, but if you are interested in this idea, or have a paper, a report, or an entry for the Bibliography that you would like to contribute to seed the database -- please send a message by return mail. If there's sufficient interest, we'll make it happen soon.

Appendix: A Job Posting

WANTED: A DESIGN VERIFICATION ENGINEER

Job Objective:
To investigate and champion the integration of formal design verification techniques into the design cycle of one of the development projects within AT&T, in one of the labs near Murray Hill in New Jersey.

Description:
The job requires the construction of a machine readable database that collects project design decisions at the earliest possible stage of a system design. The database should be compatible with existing CASE tools, and support links to verification tools such as SPIN. The formal verification framework is intended to support the entire software design cycle, from requirements analysis up to and including automated test sequence generation and assessment techniques.

Background:
Solid background in system engineering, preferably with exposure to telephony network operation systems. The ideal candidate has several years of experience being part of a system design team, and has experience with the application of formal verification techniques. Familiarity with programming languages such as C or C++, with documentation tools such as FrameMaker, and with CASE tools, are all a plus.

For more information: contact [email protected]ell-labs.com

End of Newsletter Nr. 6.