Software Testing, Verification and Validation		Karl J. Lieberherr
COM 3220						Spring 1998
===========================================================================
							Due date: May 4, 1998

This assignment is stored in file $TVV/hw/4
in file assign.txt              

=========


ASSIGNMENT 4


Whenever you have questions about course material,
please send e-mail to:

mail lieberherr@ccs.neu.edu com3220-grader@ccs.neu.edu ccs.courses.com3220@ccs.n
eu.edu                                                  

All messages which I send to the class are archived in

/proj/demsys/logs-lieber/com3220
=========        

READING:

Our text book does not seem to have much material about
testing multi-threaded programs. 
Anyway, read chapter 19 on state machines and state charts.
That contains useful material about modeling subsystems and
it even talks about communicating state machines
which can be viewed as a form of multi-threaded program.

===================================================

What to turn in:
  test requirements 
  test specifications
    indicate how your tests cover your test requirements.
    (a regression test suite; run it and show the output)
  bug reports (see earlier email message)


Testing multi-threaded programs
===========================
The code is in: $TVV/hw/4/cool

With Java it has become more popular to write multi-threaded programs.
In this homework you test two such programs.

Testing multi-threaded programs is difficult because of dependencies on the 
context of the program: load on the computer or the computers changes 
the timing behavior. Errors may only reveal themselves as failures 
in certain special situations.

PART A:
=======

The first program is a bounded stack program. There is a class
BStack which can store at most c elements and the class has a
put and a take operation to add and remove elements from the stack.

The stack is used by two threads which need to be synchronized.
The following, so called coordinator, expresses the coordination
in a high-level form:

coordinator BStack {
  selfex {put, take}
  mutex {put, take}
  put requires !(count==SIZE) 
  take requires !(count==0)  
}

SIZE is that maximal capacity of the stack.
count is a counter indicating how many elements are currently
in the stack.

mutex (put, take} means that put and take are mutually exclusive.
This means that when put is called by some thread then no other
thread is allowed to call take, and vice versa.

selfex {put, take} means that put and take are self-exclusive, i.e.,
when put is called by one thread then no other thread may call put.
The same for take.

In cool/stack and cool/stack2 and cool/stack3
are three programs which are supposed to implement
the above specification. There are two processes and one calls put 6 times
and the other calls take 6 times.

To run the programs, you copy 

/home/lieber/.www/com3220/hw/4/cool

into your directory.

To run the multi-threaded programs, for example stack,  you need 
to call 

/proj/demsys/weaver/bin/demcool

in directory stack.
(It is suggested that you put: /proj/demsys/weaver/bin/ into your UNIX path
and then you can call just "demcool".)

To run the program, you run

demjava test

Your task is to test three versions of class BStack
(in stack and stack2 and stack3). To exercise this class 
you should modify the Thread.sleep(...) calls to bring out the 
faults in the program as failures. You may also want to change 
the SIZE of the stack.

You may also want to write 
your own Java programs which gives the 
BStack class a good workout.

Each time you make a change to program.beh, you need to run again

/proj/demsys/weaver/bin/demcool

and then 

demjava test

PART B:
=======


The next class to test is the Printer class. It has two methods,
print1 and print2 which should be mutually exclusive.
Each method prints four lines and after each line it yields
to other threads.

You test 3 versions of the Printer class (print, print2, print3).
They are in $TVV/hw/4/cool

To test the Printer class, you need to adjust the timing loop

while(System.currentTimeMillis() < time+?) {}

inside print1 and print2 to reveal the faults.


PART C:
=======

This is a model checking homework and I don't know
how good the software at CMU is for this task.

Explore:
http://www.cs.cmu.edu/afs/cs/project/modck/pub/www/modck.html

Make a very simple example of a finite state machine and a very simple
CTL formula which the model checker needs to check for your
state machine. Make an example where the formula holds and one
where the formula does not hold.

Just to get the feeling for model checking.

What to turn in for part C:
the inputs you give to the CMU model checker and the outputs
it produces.