SPIN NEWSLETTER Nr. 16

SPIN NEWS - Nr. 16 - 11 March 1997

Program and Registration Information for SPIN97

    Date:     Saturday, April 5 1997
    Place:    University of Twente, Enschede, The Netherlands

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, and has inspired many other verification tools.

The SPIN97 workshop will take place following TACAS'97 (Third Intern. 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. More information about TACAS'97 can be found at URL http://wwwtios.cs.utwente.nl/~tacas97/

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) - langerak@cs.utwente.nl
    Eli Najm                    - najm@res.enst.fr
    Gerard J. Holzmann          - gerard@research.bell-labs.com

FINAL 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 can 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 bus number 1 with destination "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 is 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. If you did NOT already register for TACAS97, and plan to attend the SPIN97 workshop, please help us plan the event by filling in the form below and send it by e-mail to

           langerak@cs.utwente.nl

If you want us to make a hotel reservation for you, make sure we receive 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. . . . . . . . . . . . . . . . . . . . . . . . .
    
    --------------------------------------------------------------------

End of Newsletter Nr. 16.

Gerard J. Holzmann (gerard@research.bell-labs.com)