SPIN NEWS - Nr. 7 - August 14, 1995

Contents of this NewsLetter:

SPIN Version 2.7

There have been seven small and one large revision of the SPIN and XSPIN sources since the last newsletter. The change from 2.6 to 2.7 was the large one, and it is discussed in more detail below. To allow the dust on the latest version of the system to settle for a bit, no main new extensions of the SPIN sources will be undertaken for the next few months.

If you have downloaded a version of SPIN that is numbered:

	2.7.Beta, 2.7, or 2.7.1
in the last two weeks, an upgrade to the more stable version numbered 2.7.2 is recommended. (As perhaps is to be expected, there were some goofs in the Beta versions.)

Starting with 2.7.1 a new upgrade script will be in place to simplify the updating process.

  1. Translation from Temporal Logic to Never Claims

    Starting with Version 2.7, SPIN includes the new translation algorithm for automatically converting next-time free LTL formulae into PROMELA Never Claims (see also Newsletter 4). The implementation is based on the algorithm by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper, which is more fully described in their paper `Simple on-the-fly automatic verification of linear temporal logic,' presented at the IFIP/PSTV Conference, Warsaw, Poland, June 1995.

    To translate an LTL formula in a never claim - one can type, for instance:

    	spin -f "[] (p U (<> q))"
    
    and get the corresponding never claim printed on the standard output.

    The above option can also be combined with the -a option (to generate a verifier) as follows:

    	spin -f "[] (p U (<> q))" -a specification
    
    which will append the appropriate never claim to the specification, before generating the verifier.

    XSPIN includes a new interface to these extra SPIN options, and allows the user to enter the formula and import it into a specification. (A new Help button explains the LTL syntax requirements, operators, precedence, etc.)

  2. Computing Reachable Value Ranges

    Supported, also through XSPIN, is a new option that will compute the effectively reachable range of variable values for all variables of type bit or byte. To enable it, compile the pan.c file with directive -DVAR_RANGES, or click the corresponding button in the Validation Panel of XSPIN. Several users were able to pinpoint errors in their models with the extra feedback that is provided by this option.

  3. New Features in XSPIN

    XSPIN has a number of extra options. One is the display of a Barchart during simulations, showing the fraction of each computation that can be contributed to each active process (updated dynamically during the run). Other extras are the new support for LTL formulae, for the new compile time options, and additional Clear, Scale, and Help buttons on many of XSPIN's panels.

  4. Process Enabling Conditions

    A proctype declaration may now optionally contain a `provided clause.' For instance, the declaration:

    	active proctype A() provided (expr) { ... }
    
    makes the execution of all instances of proctype A conditional on the truth of `expr.' The expression can contain global references, or references to the process's _pid, but no references to local variables. The main drawback of using provided clauses is that it is incompatible with partial order reduction.

  5. Process Simulation Priorities

    Run statements can be given an optional priority clause, that sets the execution priority of the new process that is created. The default priority is 1 -- higher priorities can be set, for instance as follows:

    	run A() priority 3
    
    For active proctypes, the priority clause can be appended to the proctype line, just like provided clauses. (The priority specified in a run statement always takes precedence though, even if it is only the default priority.) Simulation priorities only have effect on the scheduling of process instances during random simulation runs. They cannot affect the outcome of a verification (Verification runs must report on all possible executions - not just the probable ones.)

Update on the SPIN Workshop

The workshop will be a forum for discussing and sharing experiences with SPIN. How can we help SPIN develop into a generally applicable and powerful model checking tool that is easily extendible and adaptable to both academic research goals and industrial applications.

Presentations will be given by most of the following early registrants (alphabetical order):

	Thierry Cattel, Hakan Erdogmus, Michael Ferguson,
	Patrice Godefroid, Jean-Charles Gregoire, Gerard J. Holzmann,
	Stefan Leue (to be confirmed), Fuchun Joseph Lin, Roberto
	Manione (to be confirmed), Doron Peled, Mark Staskauskas.
The presentations planned so far will focus on modeling feature interaction problems (Lin), LTL model checking and partial order reduction techniques (Godefroid, Peled), applications of bitstate hashing techniques (Staskauskas), hybrid verification (Gregoire), extensions of SPIN (Manione, Erdogmus), application experiences (Cattel), and generic extendability issues.

If you plan to attend FORTE95, do consider attending the workshop, and drop us a note so that we know roughly how many people to prepare for. We hope that participants will be vocal, present a position paper, or come ready to argue a case, but there are no requirements on participation, anyone interested in model checking is welcome.

For details on participating:

	Jean Charles Gregoire from INRS-Te'le'communications
	[email protected]

Appendix: SPINe

The following is submitted by Hakan Erdogmus, from the Software Engineering Laboratory, INRS in Canada. Hakan can be contacted by email via: [email protected]

SPINe Version 1.2b --- SPIN with relation checking

SPINe extends SPIN Version 1.5.7 with limited relation checking capability. It was developed in 1994 at INRS-Telecommunications, Montreal, Quebec.

To run SPINe do:

	spine -e[N] [fileL] [fileR]
where
	- [N] is an integer specifying the relation to be verified 
	- [fileL] and [fileR] are two PROMELA models to be compared,
called Left, and Right specifications

The above command generates a relation checker, a family of C files with prefix poc (poc for PreOrderChercker). The main file poc.c is compiled by

	cc -o poc poc.c -lm 
and the output poc is then executed to perform the desired check.

Use option

	-e1 for trace simulation (regular language containment)
	-e2 for trace equivalence (regular language equivalence)
The syntax of PROMELA has been extended to support the new capability. The new syntax allows a chan declaration to be annotated by an external name as follows:

chan [intname] (extern [extname] [btype]) = [[nslots]] of { ... }

where [intname] is the usual channel name and [extname] is the external name of the channel. Each external name must be unique in a given model. The above syntax cannot be used with an array of channels.

When a channel is declared with an external name, send and/or receive operations on that channel can be compared with similar operations of a compatible channel having the same external name in another model. Operations on external channels constitute the externally observable behavior of a PROMELA model. The [btype] field can be ? or ! or omitted:

	?	is used to declare only the receive operations on a
		channel to be externally observable.
	!	is used to declare only the send operations on a
		channel to be externally observable.
If [btype] is omitted, both sends and receives are treated as externally observable operations. For synchronous channel, either ! is specified or [btype] is omitted altogether.

Notes:

The extension is based on inductive relation checking, an on-the-fly fixpoint algorithm to verify a particular class of behavioral relations on labeled transition systems. I have identified this class (inductive relations) in my PhD thesis. It includes regular language (trace) containment and equivalence, Hennessy's must testing preorder, as well as a number of other useful relations. Unfortunately, inductive relation checking, although straightforward to implement, is PSPACE-hard. Therefore, the SPINe system suffers from the combinatorial explosion problem.

The code for verifying must testing preorder was written by a former student (Charles Cleary), but I have not tested and integrated it to the SPINe system yet. This will probably be done (provided that there is enough interest) when SPINe is upgraded to be compatible with SPIN version 2.7.

The class of inductive relations exclude such essentially stronger relations as observation equivalence (weak bisimulation) which provide a lower level of abstraction from internal transitions but which can be verified in polynomial time (although I am not aware of a polynomial time on-the-fly verification algorithm for weak bisimulation).

The purpose of this project was to assess the extensibility of SPIN with relation checking and whether this would be useful. I successfully used it to compositionally verify a small remote task protocol. If there is enough interest, I will continue to improve the existing system. Future possibilities include incorporation of polynomial relations such as observation equivalence, a port to version 2, and incorporation of complexity reduction techniques to relation checking. For example, the hide construct of PROMELA2 can be useful in reducing the complexity.

Availability

The SPINe system is available by anonymous ftp from

	zoosun.iit.nrc.ca
The relevant (tar) files can be found in the directory
	/pub/incoming/hakan
The files are as follows: Suggestions, questions, and comments are welcome. Please contact Hakan Erdogmus at [email protected]

End of Appendix.

End of Newsletter Nr. 7.