SPIN98 Workshop - Online Proceedings
SPIN98 - Papers
from the 4th International
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
Prof. Amir Pnueli
Modeling and validation of Java multi-threading applications using Spin.
Faculty of Mathematical Science
Weizmann Institute of Science, Israel
When verifying temporal properties of reactive systems, the common
wisdom is: if it is finite-state, model-check it, otherwise one must
use temporal deduction, supported by theorem provers such as STEP,
The study of abstraction as an aid to verification demonstrated that,
in some interesting cases, one can abstract an infinite-state system
into a finite-state one. This suggests an alternative approach to the
temporal verification of infinite-state systems: abstract first and
model check later.
In this talk, we explore the generality of this alternative
approach. Namely, is it the case that everything that can be verified
using temporal deduction can also be verified by abstraction followed
by finite-state model checking? We will identify classes of properties
and abstractions for which the VFA (Verification by Finitary
Abstraction) approach is sound and complete.
C., R. Iosif, R. Sisto,
[email protected], Politecnico di Torino, Italy.
Postscript: p23.pdf (15 pgs.)
Verifying Business Processes using Spin.
Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld,
Eindhoven Univ. of Technology, The Netherlands.
Postscript: sjouke.pdf (16 pgs.)
CTL* Model Checking for Spin.
Willem Visser and Howard Barringer,
Manchester University, UK.
Postscript: p6.pdf (20 pgs.)
Profiting from Spin in PEP.
Bernd Grahlmann and Carola Pohl,
Univ. of Oldenburg, SerCon Mainz, Germany.
Postscript: p7.pdf (19 pgs.)
Slicing Promela and its Applications to Protocol Understanding and Analysis.
Lynette Millett and Tim Teitelbaum,
[email protected], Cornell Univ., USA.
Postscript: millet.pdf (9 pgs.)
Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin.
Moataz Kamel and Stefan Leue,
Univ. of Waterloo, Canada.
Postscript: m2kamel.pdf (11 pgs.)
A Feature Construct for Promela.
Malte Plath & Mark Ryan,
[email protected], Univ. of Birmingham, UK.
Postscript: plath.pdf (20 pgs.)
On the fly Conformance testing using Spin.
Rene G. de Vries and Jan Tretmans,
[email protected], Univ. of Twente, The Netherlands.
Postscript: rdevries.pdf (13 pgs.)
Automatic Invariant Deduction in Spin.
[email protected], MIT, USA.
Postscript: p18.pdf (9 pgs.)
Difference compression in Spin.
[email protected], Univ. de Frache-Comte, Besancon, France.
Postscript: parreaux.pdf (7 pgs.)
Formal Analysis of a Space Craft Controller using Spin.
K. Havelund, M. Lowry, J. Penix,
NASA Ames Research Center, USA.
Postscript: p22.pdf (21 pgs.)
Analysing a basic call protocol using Promela/Xspin.
Muffy Calder and Alice Miller,
[email protected], Univ. of Glasgow, UK.
Postscript: muffy.pdf (13 pgs.)
Production Cell Revisited.
Bernd Biechele, Marsha Chechik, and Dimitrie Paun,
Univ. of Toronto, Canada.
Postscript: chechik.pdf (19 pgs.)
Formal Verification and Simulation of the NetBill Protocol Using Spin.
Jose Garcia Fanjul,
Oviedo University, Spain.
Postscript: fanjul.pdf (16 pgs.)
Elie Najm: [email protected]
Ahmed Serhrouchni: [email protected]
Gerard Holzmann: [email protected]
Online Proceedings for Previous Spin Workshops