Subject: BoF session in Prague "Formal State Machines"

From: Stephane Bortzmeyer <[email-masked]>
Date: Mon, 5 Feb 2007 21:27:03 +0100

The AD just approved the BoF session in IETF 68 in Prague:

"Formal State Machines"

http://www1.tools.ietf.org/bof/trac/wiki

See you in Prague to discuss requirments, specifications, and Unicode
characters in identifiers :-)

_______________________________________________
Cosmogol mailing list
[email-masked]
https://www1.ietf.org/mailman/listinfo/cosmogol

---

From: Hannes Tschofenig <[email-masked]>
Date: Tue, 06 Feb 2007 10:09:09 +0100

Hi Stephane,

I worked on a couple of documents that contain a state machine. For 
example,

QoS NSLP State Machine
http://tools.ietf.org/wg/nsis/draft-fu-nsis-qos-nslp-statemachine-05.txt
http://www.ietf.org/internet-drafts/draft-fu-nsis-qos-nslp-statemachine-05.pdf

NATFW NSLP State Machine
http://tools.ietf.org/wg/nsis/draft-werner-nsis-natfw-nslp-statemachine-03.txt

GIST State Machine
http://tools.ietf.org/id/draft-ietf-nsis-ntlp-statemachine-02.txt

I worked on these documents to make it easier to quickly produce a 
compliant implementation.
I have received good feedback from implementers telling me that it 
helped them a lot.

We tried to use the language introduced by the EAP state machine: 
http://tools.ietf.org/rfc/rfc4137.txt

What is difficult with the work is the lack of tool support to produce 
the PDF version of the document (or a text version from the PDF).

Why should I re-write my documents to comply to a more formal state 
machine description?

Ciao
Hannes

---

From: Stephane Bortzmeyer <[email-masked]>
Date: Tue, 6 Feb 2007 22:24:38 +0100

On Tue, Feb 06, 2007 at 10:09:09AM +0100,
 Hannes Tschofenig <[email-masked]> wrote 

> Why should I re-write my documents to comply to a more formal state

Figures (wether in ASCII-art, in Unicode-art, in SVG, in GIF or
whatever) and informal tables are impossible to analyze automatically
(for instance to check if they are deterministic, or to translate them
automatically to software like Ragel). That's the main problem I have
with informal descriptions: you cannot process them by software and
you have to check them manually.

Being parsable by a program is the main aim of the future language.

---

From: Hannes Tschofenig <[email-masked]>
Date: Wed, 07 Feb 2007 21:46:32 +0100

Hi Stephane,

I used formal languages for the verification of security protocols. I 
gave a presentation about the AVISPA project at IETF#59  (see 
http://www.tschofenig.com/avispa/).

I also applied them to some more recent protocols as well, including HIP and
http://www.tschofenig.com/svn/draft-vidya-mipshop-handover-keys-aaa/draft-vidya-mipshop-handover-keys-aaa-00.txt
(see Appendix E).

There are many nice things out there. The question is only: For whom is 
it helpful and how does it help them?

The above-mentioned formal method tool for verifying security protocols 
might help the protocol designers and people from a formal method 
community when reading IETF documents. The latter group is pretty small 
in size and regarding the former one I noticed that it only helps to the 
extend that they represent the protocol in a different way and could 
therefore discover some inconsistency in their document. The formal 
verification part is for most protocols useless since real problems are 
not discovered.

Here is my conclusion: it looks nice on paper but the tradeoff (effort 
to write compared to the value one gets) lead people to not use it.

So, coming back to the formal state machine language.

Have tried to apply your favorite language to a more complex, real-world 
protocol?
Have you been noticing real problems in the way how existing protocol 
specifications are written?
Why do you expect people to use it?
Have you spoken with implementers/protocol designers to determine 
whether you solve one of their problems?
Why do you think that the benefit is bigger than the effort?

In any case, I think that it is a useful thing to talk about this stuff 
and to give some guidance. It depends on how far you would like to go. 
If the idea is to give some guidance on how state machines could be 
described in IETF documents then that would be fine. If every working 
group suddenly has to write state machine documents using the developed 
language then some folks could get a bit nervous.

Ciao
Hannes

PS: My students have used  the following tools in past projects: the 
state machine compiler, available at http://smc.sourceforge.net, and for 
graphical representation they used 
http://www.research.att.com/sw/tools/graphviz/.

---

From: Fred Baker <[email-masked]>
Date: Thu, 8 Feb 2007 00:24:19 +0100

Having written parsers for table-described state machines, I beg to  
differ. Table-described state machines can in fact be machine- 
readable if they are designed to be. It's just another way to write  
the language.

In fact, I'll argue the flip side; SDL and compiler-compiler  
languages like YACC often fail to describe every possible input in  
every possible state. Rather, they tend to say things like "the  
receipt of this input in any other state is an error and should be  
handled in <this> way" - where the action might be "ignore the  
input", "fail, discard all accumulated state, and revert to initial  
conditions", or something else.

What is required for any state machine definition to be complete is  
that every input is described in every state, and should the input  
arrive, the resulting actions, side effects, and new state must be  
unambiguously defined. What is necessary for that to be parseable is  
that the description be understandable by an appropriately-written  
program. 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. You might prefer  
token parsers like lex. But those are matters of preference, not  
possibility.

---

From: Frank Ellermann <[email-masked]>
Date: Thu, 08 Feb 2007 20:15:21 +0100

> readable if they are designed to be. It's just another way to write

Makes sense.  But it would be nice to have a common language for such
simple cases, intuitively readable (without manual), and at the same 
time working as input for tools (validators and/or transformations
into other formats).

For something that's complex enough to _need_ SDL putting it into a
plain text 69-columns format is most probably anyway hopeless. 

Any proposal has its own limitations, but that's no reason to offer
no format suited for the publication in RFCs at all.  

> 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.

Maybe I would like it if a common format using ascii-art tables is
defined.  I won't like it if I have to tweak that program depending
on peculiar features of any individual RFC using this format.

> You might prefer token parsers like lex. But those are matters of
> preference, not possibility.

If the matter of preference starts with "you have perl / xerxes /
..." I'd say "no, not for the O/S on my box".  

Hannes Tschofenig wrote in another article:

| If every working group suddenly has to write state machine 
| documents using the developed language then some folks could
| get a bit nervous.

IMO that can't be the goal, you're also not forced to use ABNF in
cases where it's clearly unsuited.  But if you use some form of
"BNF" please don't roll your own like the horrorshow in RFC 2068,
and stick to RFC 4234 with all minor warts it still has.  Nobody
is forced to use <CHAR>, <CTL>, or the dangerous <LWSP> with its
"lines containing only trailing white space" vs. "empty lines".

Frank

---

From: Stephane Bortzmeyer <[email-masked]>
Date: Thu, 8 Feb 2007 21:45:27 +0100

On Thu, Feb 08, 2007 at 12:24:19AM +0100,
 Fred Baker <[email-masked]> 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

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?

---

From: Fred Baker <[email-masked]>
Date: Fri, 9 Feb 2007 09:24:53 +0530

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.