The Second International Spin Workshop will be sponsored by DIMACS this year -- (DIMACS is the NSF Science and Technology Center for Discrete Mathematics and Theoretical Computer Science, a consortium that includes Rutgers and Princeton University, and research labs such as Bellcore, Bell Labs, and AT&T Research). DIMACS is organizing a special year on Logic and Algorithms, and is hosting several major international conferences in New Jersey this year, such as LICS (Logic in Computer Science), and CAV (Computer Aided Verification), and a range of smaller workshops. More information on the special year can be found via URL: http://dimacs.rutgers.edu/.
As a result, the venue of our workshop will most likely move
to Rutgers University -- in the same buildings where the other
conferences and workshops will be held. It also means that
the Proceedings of the SPIN96 Verification Workshop will now
be officially published by the AMS (the American Mathematical
Society) as a book in the DIMACS series. The Proceedings will
most likely not actually appear in its final form before 1997,
but it gives welcome additional exposure to the SPIN Workshop
participants. Authors of the papers that are presented at the
workshop will have time to submit a final edited version of the
papers after the workshop itself -- details will follow when the
time gets closer.
SPIN Updates since last Newsletter
The current version of Spin is Version 2.8.
The main change, justifying the move up from 2.7 to 2.8, is that
the current version of Spin is the first one that can be used on
either generic Unix systems and on PCs. Both the Spin software
itself and the Xspin Tcl/Tk interface have been adapted to work
without change on either platform.
You minimally need working (and recent) versions of gcc and of
Tcl/Tk. Use the newest version 7.5/4.1 -- previous Windows ports
of Tcl/Tk had many internal problems that were fixed in the latest
release -- currently that is the file `win41b3.exe' which can be
obtained via anonymous ftp from ftp.smli.com in directory /pub/tcl
If you have Tcl/Tk and Gcc installed in the default places on your
PC, you can also use the precompiled version of Spin/Xspin which is
available from netlib.bell-labs.com as file: /netlib/spin/pc_spin280.zip
To compile your own version, you also need a PC version of yacc
(e.g., the public domain Berkeley Yacc version called byacc),
and can compile spin.exe with the following 3 commands:
byacc -v -d spin.y gcc -DPC *.c -o spin coff2exe spinThis port of SPIN will work on any PC system. The Tcl/Tk version of XSPIN will work on WINDOWS95 systems, but (because of remaining flaws in the Tcl/Tk Port) not yet on Windows 3.1. Once the Tcl/Tk port from SUN is bugfree, this version should work without change on any platform.
Abstract: SPIN is a tool to simulate and validate Protocols. PROMELA, its source language, is a formal description technique like SDL and Estelle that is based on communicating state machines. Unlike most other tools, SPIN is in the public domain and therefore is one of the most widely used formal verification tools today. PROMELA allows to specify distributed automata that can communicate using either message channels or shared memory. Because of the closeness to automata theory, its easy syntax and the intuitive graphical interface "xspin", PROMELA is also very suitable for educational purposes. On the other hand, SPIN offers modern algorithms for protocol validation. This contribution consists of an extension of SPIN that allows to create a compiled implementation of the specification. This can be used for testing protocols and building test scenarios. As an example for the rapid prototyping of an implementation we specify the "Alternating Bit Protocol" in PROMELA, validate it with SPIN and afterwards compile it into a distributed implementation
Abstract: Syntactical modeling of synergistic distributed systems in high level specification languages like PROMELA, its validation and simulation with start of the art tools like SPIN, is an open field in computer science. We propose an experimental and theoretical extension suitable for PROMELA/SPIN by using the semantics capabilities of PROMELA to express acceptance conditions for six types of Omega Automata (Buchi, Muller, Rabin, Streett, Kurshan, and Manna-Pnueli) with special never claim constructs. Some examples are included.
SPIN96, Second International SPIN Verification Workshop
Date: Monday, August 5, 1996
Place: Rutgers University, New Brunswick, New Jersey, USA
Duration: One day (tentatively: 9am - 5pm)
Keynote speaker: Moshe Y. Vardi, Rice University
Papers: Papers can be up to 20 pages in length and can be
either a report on work in progress or a regular
research paper on work that is somehow related to
the SPIN system.
Demos: Tool demonstrations, of extensions, restrictions
variations, or alternatives, to SPIN, are invited.
Please tell us as early as possible if you plan
to demonstrate software - so that we can make sure
we can set it up properly and make it work.
Dates: The deadline for all contributions is:
Saturday, June 15, 1996.
Papers can be submitted electronically, in PostScript
form to any one of the organizers. We will make available
a Proceedings of the workshop in both printed and also, for
the authors that permit us to do so, in electronic form.
The final workshop Proceedings will be published in book
form by the AMS in the regular DIMACS series.
Organizers:
Jean-Charles Gre'goire - gregoire@inrs-telecom.uquebec.ca
Gerard J. Holzmann - gerard@research.bell-labs.com
Doron Peled - doron@research.bell-labs.com
End of Appendices.
Gerard J. Holzmann (gerard@research.bell-labs.com)