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:
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.
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...)
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
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
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.
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 spin_list@research.bell-labs.com subscribe to spin list .
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
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 gerard@research.bell-labs.com
Gerard J. Holzmann (gerard@research.bell-labs.com)