% some global effects/font defn's
\nopagenumbers
% \parskip 1 em
% \parindent 0 em
\font\fhead = cmbx10 scaled \magstep 2
\font\fnorm = cmr10 scaled \magstep 1
\font\fbold = cmbx10 scaled \magstep 1


% useful macros

\def\mysecthead#1{ {
   \vskip 1 em\fbold\noindent
   #1
   \vskip 1 ex
 } }

\def\myreversed#1{ {
   \leftskip=20 pt
   \noindent\hang
   #1

   } }

%
% The document:
%
\fnorm
\noindent
Matthew Ogilvie\hfill\break
CS 622-1\hfill\break
May 12, 1997\hfill\break
\centerline{\fbold CFSM Test Case Generator}
\vskip 1 ex

\mysecthead{Introduction:}

For my semester project, I enhanced the project that I wrote last
semester.  Before it could do reachability analysis on communications
finite state machines (CFSMs).  The first enhancement
was to clean up the existing code (including a subtle bug fix).
Then I enhanced it so that it
can also generate test message sequences that can verify that
a protocol implementation matches its CFSM.
The code could now use another round of cleanup :).


\mysecthead{File format:}

The program recognizes four command line parameters:  -f means that the
next argument is the file name, weather it looks like an argument or not.
-u means find and
print UIO sequences for the input states.  -t means actually find a test
sequence, and -r (the default) means perform reachability analysis.  
The program needs exactly one specification file name as well.

The specification file has two types of statements:
First there are channel and message declarations, and second, there
are actual machine definitions.  An example line declaring channels
is ``channel A B C;'',
which says that you have three channels, A, B and C.  Similarly,
``message X Y Z;'' says that X, Y, and Z are possible messages that can be
send through channels.

To define a machine, the first line is ``machine machine\_name'',
where machine\_name is the name of the machine.  Then comes a block
defining the states and transitions in that machine.  It contains
``state\_name:'' followed by one or more phrases
that read ``channel + message $>$ new\_state ;''
(for receive message transition), ``channel - message $>$ new\_state ;''
(for
send message transitions), or ``timeout $>$ new\_state ;''  (for timeout
transitions.  Timeouts will only occur if there are no more then 2
messages in any channel.)  The entire block (which may have multiple
``state\_name:'' phrases) is enclosed in braces.  See one any of the
example machine files; it is easier to read an example.

The file is free-format.  It ignores white space except where it separates
keywords from identifiers.  Comments can be specified anywhere by
putting a \# sign in; it comments out everything to the end of the line.
All states, machines, channels and messages are identified with standard
symbolic identifiers; you don't have to use nondescript numbers/letters
for any of them.


\mysecthead{Reachability Analysis Mode:}

When operating in reachability analysis mode, my program can,
among other things, find unused states and transitions, identify
deadlock and unspecified reception global states, and list out the
global states.

The output consists of three parts.  The first part is a list
of all global states.  All global states are numbered.  The first
time a given global state occurs in the output, it is printed out
completely.  Subsequent references only print the ID number.
The output repeatably lists the ID number of a
global state, then lists all successors of that state.  If a state
is deadlock or UR, that fact is listed in place of the nonexistent
successors.

The second part of the output prints out the machine specification, along
with information telling, for each state and each transition, weather or
not it was ever used.

The third part lists each channel, and tells weather it was ever used
and the maximum number of messages that were ever qued up in it.
After that is a single line summarizing how many deadlock and UR states
were found.


\mysecthead{UIO and Test Sequence Generation mode:}

These modes work by simply performing the necessary calculations and
printing the results.  When outputting the sequences, the output is
directly labeled with the node transition labels.  So to actually use
it, if the sequence says the machine receives a message (with a +),
that means that you send that message to it.

One additional twist: The algorithms it uses work best when labels are of
the form (Input message/Sequence of output messages).  As a result,
only states from which the machine receives messages are considered
``real''.  So the only transitions it tests are the virtual-transitions
formed by an input followed by all implied outputs.  Also, it only
bothers to calculate UIO sequences for states that receive input.
In the description of the algorithm below, when I refer to a transition,
I actually mean its virtual-transition.


\mysecthead{Algorithm (overall):}
     The basic algorithm for generating a test case sequence is the following:

\myreversed{1) Verify that the machine is deterministic.  If it isn't,
the protocol
tester won't be able to tell which state the machine will enter next.}

\myreversed{2) Transform machine into a more convenient to work
with form.  This
more convenient form has edges that have one input (receive) transition
followed by whatever output transitions are implied from that input.}

\myreversed{3) Find Unique Input/Output sequences for each
state.  A UIO for a
state is a test sequence such that by starting from any other state and
following the sequence, at least one expect message in the sequence wont
match.  That is, only the state that the UIO belongs to will satisfy the
UIO.}

\myreversed{4) Augment with source and sink nodes.  Then add
transitions from source
node to any node with more incoming then outgoing nodes, and similarly
with sink nodes.  When calculating incoming and outgoing transitions,
count not only the original transitions, but also the ``virtual''
transitions that you get by following a transition from its start state
to the state you get to if you follow the UIO of the ``normal'' end state.}

\myreversed{5) Find min-cost max-flow for the augmented FSM.  This means
find the ``flow'' through each transition that maximizes flow to/form SOURCE
and SINK, while minimizing the total cost of all transitions.}

\myreversed{6) Build a logical graph that contains the
following transitions.  First,
it contains flow copies of each of the original transitions.  Second,
it contains the one virtual edge per original transition that goes from
initial state of the transition to the last state of the UIO of the final
state.}

\myreversed{7) Find Euler tour of the augmented FSM.  This is a tour
that visits each edge exactly once.}

     If the edge-duplicated version of the graph found in step 6 is connected
(you can get to any state from any other state), then this algorithm is
guaranteed to find the shortest test sequence that tests all transition with
UIO sequences.

     However, it is possible that the graph is not connected.  As currently
implemented, the algorithm doesn't work in this situation: It prints and
error message and calculates a tour of one connected region only.



\mysecthead{Deterministic:}

     Checking weather the machine is deterministic is fairly easy.  All you
need to do is check to make sure that the outgoing transitions from a state
satisfy one of the following conditions:
\myreversed{1) Exactly one SEND transition is there.}
\myreversed{2) There are multiple RECV transitions, but at most one from
 any unique
channel/message type pair.  There may also be at most one TIMEOUT transition.
However, no SEND transitions are there.}


\mysecthead{Unique Input/Output sequences algorithm:}

     This algorithm works by trying progressively longer sequences until
the number of actions in the sequence reaches 2*((number of nodes)**2).
When trying a sequence, it checks two things: First, if the sequence isn't
satisfied when starting from any other state in the machine, then an
UIO has been found, and the algorithm stops.  Second, if when starting from
any other state the final state is the same as the final state starting
from the state we are working on, then no sequence that has this sequence as a
prefix will work, and we can drop any further consideration of any
sequence that has this sequence as a prefix.

As an optimization, length l sequences are constructed from length l-1
sequences.

     If there are no more valid prefixes, or the length of the sequence
gets too long, then there is no UIO for that state, and you must use
some less satisfiable sequence.  The program currently picks one of the
longer failed potential UIOs.


\mysecthead{Minimum-cost Maximum-flow (Ford-Fulkerson) Algorithm:}

     This algorithm works by repeatably finding least-cost paths from source
to sink with spare capacity.  As it looks for paths with capacity, it
not only looks for paths in forward direction that aren't maxed
out, it also looks for paths in negative direction that have
non-zero flow that can be reduced.  When a path is found, it changes the
flows to the new values.  When no more paths can be found, the max-flow
min-cost path has been found.


\mysecthead{Euler tour algorithm:}

     This algorithm works by repeatably finding a circular path through
the graph, and splicing it into the Euler tour, until all transitions are
traversed in the Euler tour.  The paths are found with a simple depth-first
search, and always start from a node in the existing tour that has
untraversed transitions incident on it.

\mysecthead{Files:}

The source code can be accessed in ``\~{}mmogilvi/cs622/proj/''.  analize.cpp
holds the meat of the program.  Most of the code for test case generation
is near the end of the file.

     The other *.cpp files are packages I've
written before.  symbol.cpp is a package that maps strings to unique
ID codes.  memgroup.cpp is a package that allows memory to be
allocated in ``groups'' that can be freed all at once.  It handles two
allocation scenarios: constant-size objects in a group that are regularly
being freed and allocated, and variable sized objects that are never
freed except as a group.  Currently it is only used by symbol.cpp, but
one enhancement would be to replace some object's new and delete with
stubs that call this package.

The *.m files are example machines designed to demonstrate
the reachability analyzer.  The file test.t is designed to test the
test case generator.  It is the same as the machine I demonstrated in class.
I may add more *.t files soon.

writeup\_mcsm.tex is the \TeX source for this writeup.  writeup.tex is
the original writeup from the original project.


\mysecthead{Future Improvements:}

Some possible improvements to this utility include the following:

\myreversed{1) Clean up the code:  This includes making the code
easier to read, as well as using better, faster
and more modular data structures.  Also, break analize.cpp into at
least 3 files: input.cpp, reachable.cpp, and testcase.cpp.}

\myreversed{2) Try to pick the best possible UIO substitute for a state
if the UIO doesn't exist.  The current method can pick some pretty unusable
values.}

\myreversed{3) Provide an easy to use interface so that communications
modules that can communicate with real implementations can be easily added.
The program would then automatically run the test script, not just display
it.}

\myreversed{4) If the graph to be traversed by the Euler algorithm isn't
connected, then somehow add enough transitions to make it connected.  The
current behavior of simply stopping isn't acceptable.}

%\mysecthead{Conclusion:}
%

\mysecthead{References:}

\myreversed{1) Weiss, Mark Allen. ``Data Structures and Algorithm Analysis
in C.''  Redwood City, CA: Benjamin/Cummings, 1993. pp 322-330.}

\myreversed{2) Kershenbaum, Aaron.  ``Telecommunications Network Design
Algorithms.'' New York: McGraw-Hill, 1993. pp 169-176.}

\myreversed{3) Dahbura, Anton and Sabnani, Krishan.  ``A protocol Test
Generation Procedure.'' ``Tools for Analysis and Synthesis of Protocols.''
Murray Hill, NJ: AT\&T Bell Laboratories, 1988.}

\myreversed{4) Aha, Alfred, Dahbura, Anton, Lee, David and Uyar, M.
``An Optimization Technique for Protocol Conformance Test Generation
Based on UIO Sequences and Rural Chinese Postman Tours.'' AT\&T Bell
Laboratories.}

\bye
