Re: BoF session in Prague "Formal State Machines"

[Fred Baker <fred at cisco.com>]

Personally, I have used a fairly convoluted series of steps in  
designing state machines for various things; I have done it because I  
found the results useful. It uses a combination of a compiler- 
compiler language and a table-driven state machine.

Let's take an intentionally complex example: TCP. A TCP session can  
be described as starting from and ending in the initial state of "no  
connection". From the initiator's perspective, there is a sequence  
(be gentle on me, I'm doing this from memory while waiting for a  
meeting to start)

	initiate:
		user-open {send SYN, start dead timer, start retransmit timer}
		[retransmit-timer {send SYN, restart retransmit timer}]*
		( dead-timer {FAIL} | network-SYN-ACK {send empty data segment,  
restart dead-timer, restart retransmit timer )

the receiver has the opposite sequence starting with the receipt of a  
SYN segment from the network and ending with either the dead-timer or  
receipt of a subsequent segment.

Constructing these rules and running them through YACC with the  
correct set of options gets me a state machine that is quite a bit  
more complex than the one in RFC 793 but in fact handles all the  
issues that a TCP implementation faces. The one change one makes to  
that state machine is changing reduction rules to jumps to the state  
that the reduction rule would place you in.

The problem with it is statements like "{FAIL}". The constructed  
state machine tells one all the necessary states and all of the  
correct state transitions; it doesn't tell much about the error  
cases. For this, I wind up transcribing the YACC-produced state  
machine into a state table and filling in all of the error cases.

I'm about to make a statement that, while it is true, will sound  
preposterous. I assure you that it is true. In 1983, working at  
Control Data, I designed an XNS SPP implementation that used what  
today we call VJ congestion avoidance procedures. I spent a lot of  
time getting the state machine correct. I then constructed a set of  
'sed' processes (we were running unix v6 on a PDP 11/34) that did  
text edits to convert my state machine into the high level code for  
the protocol, and wrote a "language" of supporting routines; the  
counterpart to "send SYN" was, for example, a call to a routine that  
constructed a control packet to be sent to the peer with a certain  
set of calling parameters.

Work that followed on that code related to optimization and setting  
parameters appropriately, but folks who later maintained it told me  
that they never found a protocol bug in it.

Identifying and ensuring the correct handling of all the error cases  
is as important, perhaps more so, as handling the normal-and-correct  
transitions. I can't say I have ever found a language that does that  
well, including and perhaps especially SDL.

On Feb 9, 2007, at 2:15 AM, Stephane Bortzmeyer wrote:

> On Thu, Feb 08, 2007 at 12:24:19AM +0100,
>  Fred Baker <fred at cisco.com> wrote
>  a message of 50 lines which said:
>
> > Table-described state machines can in fact be machine- readable if
> > they are designed to be.
>
> Nobody ever said the opposite. Cosmogol is very close from a
> table-described state machine, by the way, although the syntax is very
> different from a typical table but a table, or a Comogol description
> are both just a list of tuples (current-state, transition,
> next-state).
>
> > Now, you might not *like* to write programs that recognize ascii-art
> > cells and find in them things like input names, new state names,
> > conditionals, actions, and side-effects.
>
> Indeed. I challenge you to write a parser for the state machines of  
> RFC
> 4006 :-) specially with the RFC headers and footers.
>
> We certainly could imagine a more table-like formal syntax with
> delimiters like:
>
> OPEN   | Close it    | CLOSED
> CLOSED | Open it     | OPEN
> OPEN   | Blow it out"| GONE
>
> (or TeX's & sign)
>
> or with fixed-size cells like RFC 4006 attempts to do.
>
> Do you find it better?

_______________________________________________
Cosmogol mailing list
Cosmogol at ietf.org
https://www1.ietf.org/mailman/listinfo/cosmogol