SPIN NEWS - Nr. 5 - May 8, 1995

Contents of this NewsLetter:

Statistics - Domain Names

In the category of idle statistics ... a quick count of email domain names shows that the subscribers to the SPIN Newsletter are spread over no less than 22 different countries. About 40% of the subscribers are from the U.S., about equally divided between companies (.com) and universities (.edu). 30% has an email destination in Europe, 13% in Canada, and 17% lives elsewhere (australia, new zealand, south africa, hong kong, israel, japan, taiwan, venezuela).

A New Language Feature in Promela

There have been nine small upgrades of the SPIN sources since the last newsletter. The current version is 2.3.4 dated May 1 1995. Starting with version 2.3.0 a new type of receive operation is supported for asynchronous message channels: the channel poll operator.

Together with random receive and channel testing, this now makes for a total of six different ways to perform a receive operation on an asynchronous message channel. The six are listed below, with a brief explanation of their purpose. The last two operations in this list are new.

  1. q?var1,const,var2 or q?var1(const,var2)
    the standard fifo receive, where any field can be either a constant or a variable-name. all constant fields must be matched by the incoming message, for the receive to be executable. if this operation is executed, the oldest message is removed from the channel.
  2. q??var1,const,var or q??var1(const,var2)
    the random receive operation that was first introduced in version 2.0. the semantics are as in (1), but in this case any message stored in the channel can be matched, it is not required to be the oldest one as in (1). if this operation is executed, the oldest message that matches (not necessarily the oldest message stored) is removed from the channel
  3. q?[ var1,const,var2 ]
    the standard boolean test of executability of a receive operation of type (1). this is a condition that can be evaluated without side-effects, and it can therefore be used freely inside expressions. the state of the channel is the same before and after this condition is evaluated.
  4. q??[ var1,const,var2 ]
    as (3), but this time the condition is true iff the corresponding receive operation of type (2) is executable. again, the condition can be evaluated without side-effects.
  5. q?<< var1,const,var2 >>
    a new operation that is called a `fifo poll' it behaves as an operation of type (1), with just one difference: when executed, no message is removed from the channel. the effect is that all variables are set to the value of the corresponding fields of the message stored in the channel, but the channel contents itself is not disturbed. the operation has side-effects (on the variables), so it cannot be used inside expressions like (3).
  6. q??<< var1,const,var2 >>
    new operation called `random receive poll' it behaves as an operation of type (2), again with the one difference that no message is removed from the channel when this operation is executed. it cannot be used inside expressions, for the same reason as (5).
Of course, channel poll operations do not work on synchronous channels. (Messages cannot be stored inside a synchronous channel; they are always passed instantly from sender to receiver in a rendez-vous handshake.)

Frequently Asked Question

Modeling Conditional Rendez-Vous Operations

The question has come up several times how one can faithfully model rendez-vous operations as they are used in, for instance, the ADA language. Unlike for asynchronous operations, as illustrated above, there is no boolean test or poll operation in Promela for synchronous receives. The reason is lies in the semantics of the rendez-vous operation itself. A complete rendez-vous operation is defined to be indivisible: there is no system `state' the would correspond to the point in between the send and the receive half of the rendez-vous handshake, where the receiver could test or poll the contents of the message channel.

Consider the sample rendez-vous arrangement:

	global:		chan port = [0] of { mtype, int };
	sender:		port!mesg(12)
	receiver:	port?mesg(data)
Now suppose we want to define an extra boolean condition P that must be fulfilled before the rendez-vous send operation becomes executable, and a boolean condition Q that must hold before the matching receive also becomes executable and the handshake can take place. It is not easy to achieve this effect with atomic sequence. Trying:
	sender:		atomic { P -> port!mesg(12) }
	receiver:	atomic { Q -> port?mesg(data) }
would be incorrect, because the sequence is just guarded by the condition, and may block in both cases after the guard is passed. The executability of the send or receive cannot be tested within the guard of the atomic.

Another strategy is needed. The following solution requires the definition of 2 additional channels, but since rendez-vous channels do not take up any memory in the verification process this imposes no overhead during verifications.

	global:		chan port[3] = [0] { mtype, int };
	sender:		port[(1-P)]!mesg(12)
	receiver:	port[(2-Q)]?mesg(data
Note that when P evaluates to false (or 0), the sender will attempt to handshake on port[1], and when Q evaluates to false, the receiver will attempt to handshake on port[2]. Only when both P and Q evaluate to true (or 1) can the sender and receiver find each other on port[0].

The First SPIN Users Workshop is On

When:

October 16th, Montreal, QC (just before FORTE'95)

Topics:

Applications of SPIN to industrial projects; possible extensions (test sequence generation, generating C code implementations, new graphical front-ends, hierarchical structures, bisimulation proofs, refinement proofs, links to theorem provers, hardware design tools, etc.)

For More Information, Suggestions, Participation:

Jean Charles Gregoire from INRS-Te'le'communications
gregoire@inrs-telecom.uquebec.ca

See Also:

Newsletter 4

Appendix 1: A Useful Shell-script (by Ted Ewanchyna)

Problem:

Replaying a simulation scenario produced interactively with SPIN option `spin -i' using the Tcl tool `Expect'

Description:

Whenever I want to replay an interactive session with spin, I first record everything with the Unix command 'script'. I then run spin -i as usual. Then I exit the script program which produces the typescript file. Then I run the awk script I wrote with the script produced filename as its only argument and it produces an 'expect' script which then reruns my interactive trace for me automatically. It only works for spin not xspin, because I don't know how to invoke the tk menus from the script. I may just put a pause in the expect script and call up the interactive simulation mode 'manually' and then throw the input at it.

Usage:

Typing 'exp.awk ' produces an executable file named '.inter'. Running that file will reproduce the last interactive session. Control is handed back to the user once the script ends.
This is the contents of exp.awk:
 #!/bin/sh
 sed '1,$s;;;g' $* |
 awk '
 BEGIN {print "#!/usr/loca./binexpect -f";print "spawn spin -i test-fc.pr"}
 /Select\ \[.*\]:*/ {
 printf ("expect {");
 for (i = 1; i < NF; i++) printf ("%s ",$i);
 printf ("}\n");
 printf ("exp_send \"")
 printf ("%s\\n\"\n",$i)
 }
 END {print "interact"}
 ' > $*.inter
 chmod +x $*.inter
Contact: tede@alcor.concordia.ca

Appendix 2: Spin Project Description (by Thierry Cattel)

Project:

Specification, Verification and Implementation of a Production Cell Controller at Ecole Polytechnique Federale de Lausanne, Laboratoire de Teleinformatique, using Promela/SPIN.

Implementation language:

Synchronous C++

Period:

January 1, 1995 - (June 30, 1995)

Size:

The PROMELA models are about 2000 LOC. The Synchronous C++ programs are about 3000 LOC. The effort was about 6 months/man.

Background:

In order to demonstrate the benefits of formal methods for industrial applications, and to evaluate and compare existing approaches for constructing and verifying control software for reactive systems, FZI launched the Case Study Production Cell in 1993 as an activity inside the German Korso Project.

Several approaches have already been applied and lead to succesfull Contributions. We have applied our own method using Promela/SPIN The implementation derived from the Promela models is written in our concurrent extension of C++: Synchronous C++.

Findings:

Promela/SPIN was initially designed for protocol modeling and verification, but it is also very adapted to distributed systems analysis as well as Operating systems' (See our contribution to Harmony in Newsletter 2). The controller is able to accept upto 8 blanks in the cell. The safety properties have been partially verified :
  • no deadlocks of any kind before 9 blanks
  • no unreached code
  • no unspecified message reception
  • cell element mobility restriction
  • collisions
  • blanks distant.
The liveness property, as appearing in the task description document has been verified for the whole cell and the whole cycle, as well as weaker forms for each cell element or subset of elements in loop.

As forecast, Promela/SPIN appeared to be also very suitable for the design of process control. (See incoming report for more details)

Relevant publications:

Cattel, T., Mesbahi A. Specification, Verification and Implementation of a Controller for the ZFI Production Cell Controller. Technical Report, EFPL, Lausanne, Switzerland. June, 1995. Will be soon available by FTP at ltidec1.epfl.ch
file: /pub/spin/papers/prodcell.ps

The FTP server ltidec1.epfl.ch /pub/spin/prodcell/spin and /pub/spin/prodcell/scpp will soon contain respectively the PROMELA models and the Synchronous C++ source code of the executable controller.

Contacts:

	Thierry Cattel
       	E-mail:  cattel@di.epfl.ch
       	Phone:   +41(21) 693 67 76 (Central European Time)
       	Fax:     +41(21) 693 66 00
       	WWW:     http://ltiwww.epfl.ch/~cattel

	Adil Mesbahi
	mesbahi@di.epfl.ch or mesbahi@rubis.iie.cnam.fr

End of Newsletter Nr. 5.

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