SPIN98 Workshop - Online Proceedings

SPIN98 - Papers from the 4th International SPIN Workshop

The SPIN98 workshop was held on Monday November 2, 1998, the day before IFIP FORTE/PSTV98, at ENST in Paris, France. Below is the list of papers presented at the workshop, in order of presentation, with links to the postscript for online versions where available.

  • Keynote: Verification by Finitary Abstraction
  • Modeling and validation of Java multi-threading applications using Spin.
    C., R. Iosif, R. Sisto, sisto@polito.it, Politecnico di Torino, Italy.
    Postscript: p23.ps.gz (15 pgs.)
  • Verifying Business Processes using Spin.
    Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld, Radu.Mateescu@cwi.nl, Eindhoven Univ. of Technology, The Netherlands.
    Postscript: sjouke.ps.gz (16 pgs.)
  • CTL* Model Checking for Spin.
    Willem Visser and Howard Barringer, visserw@cs.man.ac.uk, Manchester University, UK.
    Postscript: p6.ps.gz (20 pgs.)
  • Profiting from Spin in PEP.
    Bernd Grahlmann and Carola Pohl, Grahlmann@informatik.uni-oldenburg.de, Univ. of Oldenburg, SerCon Mainz, Germany.
    Postscript: p7.ps.gz (19 pgs.)
  • Slicing Promela and its Applications to Protocol Understanding and Analysis.
    Lynette Millett and Tim Teitelbaum, millett@cs.cornell.edu, Cornell Univ., USA.
    Postscript: millet.ps.gz (9 pgs.)
  • Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin.
    Moataz Kamel and Stefan Leue, m2kamel@uwaterloo.ca, Univ. of Waterloo, Canada.
    Postscript: m2kamel.ps.gz (11 pgs.)
  • A Feature Construct for Promela.
    Malte Plath & Mark Ryan, M.C.Plath@cs.bham.ac.uk, Univ. of Birmingham, UK.
    Postscript: plath.ps.gz (20 pgs.)
  • On the fly Conformance testing using Spin.
    Rene G. de Vries and Jan Tretmans, rdevries@cs.utwente.nl, Univ. of Twente, The Netherlands.
    Postscript: rdevries.ps.gz (13 pgs.)
  • Automatic Invariant Deduction in Spin.
    Mandana Vaziri, vaziri@theory.lcs.mit.edu, MIT, USA.
    Postscript: p18.ps.gz (9 pgs.)
  • Difference compression in Spin.
    Benoit Parreaux, parreaux@lib.univ-fcomte.fr, Univ. de Frache-Comte, Besancon, France.
    Postscript: parreaux.ps.gz (7 pgs.)
  • Formal Analysis of a Space Craft Controller using Spin.
    K. Havelund, M. Lowry, J. Penix, havelund@ptolemy.arc.nasa.gov, NASA Ames Research Center, USA.
    Postscript: p22.ps.gz (21 pgs.)
  • Analysing a basic call protocol using Promela/Xspin.
    Muffy Calder and Alice Miller, muffy@dcs.gla.ac.uk, Univ. of Glasgow, UK.
    Postscript: muffy.ps.gz (13 pgs.)
  • Production Cell Revisited.
    Bernd Biechele, Marsha Chechik, and Dimitrie Paun, chechik@cs.toronto.edu, Univ. of Toronto, Canada.
    Postscript: chechik.ps.gz (19 pgs.)
  • Formal Verification and Simulation of the NetBill Protocol Using Spin.
    Jose Garcia Fanjul, fanjul@lsi.uniovi.es, Oviedo University, Spain.
    Postscript: fanjul.ps.gz (16 pgs.)

    Workshop Organization

       Elie Najm: Elie.Najm@Email.ENST.fr
       Ahmed Serhrouchni: ahmed@res.enst.fr
       Gerard Holzmann: gerard@research.bell-labs.com	

    Online Proceedings for Previous Spin Workshops

    Spin homepage: http://netlib.bell-labs.com/netlib/spin/whatispin.html