This directory contains files for Technical Report CSRI-388.

The files in this directory are the following:

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

If you have the UNIX "gunzip" program, get the file TR-388.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-388.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:    Automatic Analysis of Consistency between Requirements and Designs

AUTHORS:  Marsha Chechik and John Gannon


ABSTRACT:

Writing requirements in a formal notation permits automatic assessment
of such properties as ambiguity, consistency, and completeness.
However, verifying that the properties expressed in requirements are
preserved in other software life cycle artifacts remains
difficult. Most of the proposed techniques suffer from exponential
explosion of the number of states in the generated state spaces. One
way to cope with this explosion is to develop and apply
``light-weight'' formal methods that will attempt to achieve
scalability by checking an abstraction of the system for only some
non-trivial properties. This paper describes methods and tools for
automatically analyzing the consistency of software requirements and
detailed designs in low-degree polynomial time. Requirements describe
systems as state machines with event-driven transitions using a
specification language that is easy to read and scalable to large
systems. We define requirements and detailed designs to be consistent
if they contain exactly the same transitions. We have developed a
language for specifying detailed designs, an analysis technique to
create a model of a design through data-flow analysis of the language
constructs, and a method to automatically generate and check
properties derived from requirements to ensure a design's consistency
with them. These ideas are implemented in a tool named CORD, which we
used to uncover errors in designs of existing systems.