This directory contains files for Technical Report CSRI-387.

The files in this directory are the following:

1) README       (< 1   KB - the ASCII file you are now reading)
2) TR-387.ps    (278.5 KB - PostScript)
3) TR-387.ps.gz (62    KB - PostScript compressed with the program "gzip")

If you have the UNIX "gunzip" program, get the file TR-387.ps.gz.
Remember to transfer the file in binary mode. After the transfer, 
"gunzip" the file.

If you do not have the UNIX "gunzip" program, get the file TR-387.ps 
in ASCII mode. 

After transfering the file, print it on a PostScript printer.

If you have any questions or comments about this technical report, please
contact chechik@cs.toronto.edu


TITLE:    Production Cell Revisited

AUTHORS:  Dimitrie Paun, Marsha Chechik and Bernd Biechele


ABSTRACT:

This paper presents an analysis of the Production Cell system. We were
able to model the system and verify most of its properties in
Promela/SPIN.  Our model is very close to the implementation level,
and deriving code from it is trivial. In order to verify properties
with SPIN's partial order reduction algorithms, we needed to ensure
that all of our properties are closed under stuttering. We introduce
the notion of logic edges and use them to show that properties of
interest to us are closed under stuttering.