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.1in 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.
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 specificationwhich 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.)
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.
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.
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.
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 3For 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.)
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 gregoire@inrs-telecom.uquebec.ca
The following is submitted by Hakan Erdogmus, from the Software Engineering Laboratory, INRS in Canada. Hakan can be contacted by email via: Erdogmus@iit.nrc.ca
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 -lmand 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.
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.
The SPINe system is available by anonymous ftp from
zoosun.iit.nrc.caThe relevant (tar) files can be found in the directory
/pub/incoming/hakanThe files are as follows:
End of Appendix.
Gerard J. Holzmann (gerard@research.bell-labs.com)