Monday November 2, 1998The workshop chair is Elie Najm from ENST, who is also general chair of FORTE_PSTV98. See: http://www-lor.int-evry.fr/~stan/FORTE_PSTV98/
The workshop is a forum for discussing and sharing experiences with the Spin model checker. It is a meeting place for all those who work on (1) the theoretical foundation of computer aided verification, (2) applications of Spin model checking to problems of practical significance, (3) empirical studies of the relative effectiveness of different types of search algorithms and memory management techniques for model checking, tool comparisons, etc., and (4) significant extensions or modifications of the basic system.
The submission deadline for papers is
Thursday August 20, 1988,
but we ask authors to send us a brief abstract, or
demo and tutorial proposals, no later than Saturday June 20, 1998.
We look forward to your contribution!
chan STDIN; /* requires Spin version 3.1 or later */
init {
int c, nl, nw, nc;
bool inword = false;
do
:: STDIN?c ->
if
:: c == -1 -> break /* EOF */
:: c == '\n' -> nc++; nl++
:: else -> nc++
fi;
if
:: c == ' ' || c == '\t' || c == '\n' ->
inword = false
:: else ->
if
:: !inword ->
nw++; inword = true
:: else /* do nothing */
fi
fi
od;
printf("%d\t%d\t%d\n", nl, nw, nc)
}
Added are also the errata for the book (most have been fixed in the online version): http://cm.bell-labs.com/cm/cs/what/spin/Doc/Errata91.txt
Another Type of Spin
Found on the web, a reference to an operating system with a
familiar name:
http://www.cs.washington.edu/research/projects/spin/www/
Title: Specification and Verification of an Object Request Broker Author: Grégory DUVAL Computer Networking Laboratory Ecole Polytechnique Fédérale CH-1015 Lausanne, Switzerland Email: duval@epfl.ch Url: http://ltiwww.epfl.ch/~duval http://diwww.epfl.ch/w3lti Contents: This paper reports the results of specifying, modeling and verifying a safe Object Request Broker. This method has been applied on several case studies by using SPIN. An object request broker has been implemented using sC++, a concurrent extension of C++ designed by our team. Liveness and safety properties have been checked on the model to ensure the system behaviour is correct. This application shows the efficiency of using formal methods in building safe applications. It also shows that sC++ is appropriate for developing protocols and communicating systems and is easily translatable from models such as Promela.
Title: Modeling and Verification of sC++ Applications Author: Thierry Cattel Computer Networking Laboratory - LTI Swiss Federal Institute of Technology CH-1015 Lausanne, Switzerland Publication: Proc. TACAS'98, April 98, Lisbon. Email: cattel@epfl.ch Url: http://ltiwww.epfl.ch/~cattel http://diwww.epfl.ch/w3lti Contents: Presents a means to model and verify concurrent applications written in sC++, which is an extension of C++ that adds concurrency by unifying object and task concepts into socalled 'active objects.' We show how sC++ programs can be modeled in Promela, a formal language supported by SPIN. We present a classical example of a concurrent problem and give details about a tool that automatically produces the model from the program, verifies it and allows its debugging.
Title: Pragmatics for Feature Interaction Author: Franck Cassez and Ahmed Bouabdallah IRCyN (UMR CNRS 6597) / ECN B.P 92101 44321 NANTES CEDEX 03 Email: lan.ec-nantes.fr!Franck.Cassez Url: http://www.cs.bham.ac.uk/~mcp/fireworks/publications.html Contents: Describes ongoing work that is part of an ESPRIT WG called FIREworks, studying feature integration. The paper describes a method for integrating features and detecting feature interactions using Promela/SPIN.
Spin (spin_list@research.bell-labs.com)