SPIN97 Workshop

SPIN97

Third International SPIN Workshop

Call for Participation

Date:     Saturday, April 5 1997
Place:    University of Twente, Enschede, The Netherlands 
Duration: One day (9am - 5pm)

SPIN is a reachability analysis tool designed for the general verification of distributed systems. First made available publicly in 1991, SPIN is widely used both for teaching and for industrial applications. It has inspired many other tools in various ways.

The first two SPIN workshops, held in Montreal (16 October 1995) and New Jersey (5 August 1996), created opportunities for SPIN users to meet and exchange experiences, ideas, theories, wishes, gripes about formal verification tools.

The SPIN97 workshop will take place following TACAS'97 (Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems), that will take place at the University of Twente on April 2-4 1997. The aim of TACAS'97 is to bring together researchers and practitioners interested in the development and application of tools and algorithms for specification, verification, analysis and construction of distributed and embedded systems. See http://wwwtios.cs.utwente.nl/~tacas97/ for more information.

The SPIN97 workshop will be held at the University of Twente, April 5 1997.

KEYNOTE SPEAKER: Prof. Pierre Wolper (University of Liege)

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.

PROGRAMME COMMITTEE:

	Rom Langerak (Organization)       - [email protected]
        Gerard J. Holzmann                - [email protected]
        Eli Najm                          - [email protected]

PROGRAM:

8.30 -- 8.50	Registration
8.50 -- 9.00    Opening

9.00 -- 10.00   Keynote Presentation by
                Pierre Wolper (University of Liege):
		Where could SPIN go next? A unifying approach
	 	to exploring infinite state spaces.

10.00 -- 10.30 	Gerard J. Holzmann (Bell Laboratories):
                State Compression in SPIN: Recursive Indexing and
		Compression Training Runs.

10.30 -- 11.00  BREAK

11.00 -- 11.30  Hans van der Schoot (University of Ottawa):
		Partial-order verification in SPIN can be more efficient.
11.30 -- 12.00  William R. Bevier (Computational Logic, Inc):
                Towards an Operational Semantics of PROMELA in ACL2.
12.00 -- 12.30  Carsten Weise (Aachen University of Technology):
		An incremental formal semantics for PROMELA

12.30 -- 13.30 	LUNCH

13.30 -- 14.00 	Siegfried Loeffler, Ahmed Serhouchni (ENST, Paris):
             	Creating a Validated Implementation of the Steam Boiler
		Control.
14.00 -- 14.30 	Erich Mikk, Yassine Laknech, Michael Siegel
		(Christian-Albrechts University at Kiel):
		Towards efficient model checking Statecharts:
		A Statecharts to Promela Compiler.
14.30 -- 15.00 	Tadashi Nakatani (Toshiba Corporation, Japan):
                Verification of Group Address Registration Protocol
		using PROMELA and SPIN.

15.00 -- 15.30 	BREAK

15.30 -- 16.00 	Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi,
		Dario Romano, Fernando Torielli, Paolo Traverso (IRST
		Trento, ASF Genova, ATR Genova):
		Model Checking Safety Critical Software with SPIN:
		an Application to a Railway Interlocking System.
16.00 -- 16.30 	Peter van Eijk (Utrecht University, EDS):
                Verifying Relay Circuits using State Machines.
16.30 -- 17.00 	Theo Ruys, Rom Langerak (Twente University):
                Validation of Bosch' Mobile Communication Network
		Architecture with Spin.

COST:

Even though workshop attendance includes proceedings, coffee breaks and lunch, attending the workshop is FREE. We kindly ask you to register in advance so we can guarantee enough proceedings and lunches.

LOCATION, AND HOW TO GET THERE:

The workshop will be held in the CC building ("Collegezalen Complex") on the campus of the University of Twente, Enschede. The porter at the entrance of the campus may tell you how to get there. The following information may be useful:

 * Train. There is a train almost every half hour between Schiphol
      International Airport and Enschede. Some services require
      you to change trains (at Amersfoort and/or Hengelo).
      Once you are in Enschede, you can walk (or catch a taxi)
      to the hotel.
 * Bus. If you wish to go by bus from Enschede (railway)
      station to the university campus, then you need to catch
      bus number 1 (the destination is "universiteit").
      This service travels every 15 minutes during the day from
      the station to the campus.
 * Car. The university is well-signposted from all directions.
      (It lies half way between Hengelo and Enschede.)
 * Taxi. Taxis are available at the train station, of course.

ACCOMMODATION AND TRANSPORT:

We have made a block-booking for participants at the DISH Hotel. The DISH Hotel is situated in the center of Enschede, and is within easy walking distance of the railway station (approx. 10 minutes across town). Hotel registration can be completed as part of the workshop registration, but hotel payment should be made at the hotel itself. The address of the DISH Hotel is:

  DISH Hotel
  Boulevard 1945 2                  tel: +31 (0)53 486 6666
  7511 AE Enschede, The Netherlands fax: +31 (0)53 435 3104

The 3-star rooms cost Dfl 100 per night; breakfast (Dfl 17.50) is NOT included in the price. If you want us to make your hotel reservation please register before 21 March (after that date rooms are not guaranteed).

There will be a free shuttle-bus service between the hotel and the university on the day of the workshop. The university is approximately 4 kilometers out of town.

REGISTRATION:

If have have also registered for TACAS97 and indicated your interest for the SPIN97 workshop, you do not have to register again for SPIN97. So please only register if you did NOT register already for TACAS97 !

Fill in the form below and send it by e-mail to

           [email protected]

Remember, if you want us to make a hotel reservation, send this form before 21 March.

--------------------------------------------------------------------
           SPIN97 WORKSHOP AND HOTEL REGISTRATION FORM
       University of Twente, The Netherlands, April 5, 1997
--------------------------------------------------------------------

Surname. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Initials . . . . . . . . . . . Title . . . . . . . . . . . . . . . .

Company/Affiliation. . . . . . . . . . . . . . . . . . . . . . . . .

Address. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

       . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Postcode . . . . . .  City . . . . . . . Country . . . . . . . . . .

Telephone. . . . . .  Fax. . . . . . . . E-mail. . . . . . . . . . .


Hotel accommodation (To be paid at the hotel.)
-------------------

 Not necessary [ ] 

 Yes, nights:    Fri. 4th    Sat. 5th
                   [ ]         [ ]

Dietary restrictions. . . . . . . . . . . . . . . . . . . . . . . . .