Lambda the Ultimate

While its focus was on formal verification and modelling, I recollect some efforts to generate SDL code from the FSMs.

There's a literature coming out of temporal logic on the declarative specification of concurrent processes and protocols that seems to drive a lot of work in the agents field. The little idea that led to it all seems to be Thiagarajan and Walukiewicz's 1997 "An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces" [Citeseer | context]; follow the links on the context page to see the material applied to protocols. I don't know of any analyses of important IETF standards using this stuff, but it's not unlikely to be there if you look for it.

i've only seen one protocol that was specified at such a level that it could be transliterated directly into source that was useful. most specifications have alot of implied semantics that take substantial thought and discussion to eek out.


however, thats not what you asked really. i did a system at tenuki.org which i think made a nice cut at the problem by:

• projecting packet field encodings directly into the environment
• providing mechanisms for encapsulation
• expressing the algorithm directly as a cfg

but of course it never left the interpreted prototype stage.


i dont think there is anything specific about protocols that make them must different than other DSL applications, but you're right, there is enough leverage there that there should really have been more work.


i assume you're familiar with Sean O'Malley's USC and
other stub-generation kind of tools, but they are really insufficient. you really want to be able to deal with recursive encapsulation, timers, optional headers, and other important concepts.


one important generalization is that fields should be bit-indexed. this causes a certain amount of endian confusion and is an interesting (but quite tractable) compilation problem in and of itself.


you should also look at Eddie's thesis work 'Click',
which is more of a system for composition than a language, but is interesting. please post if you find anything cool.

Peter Sewell's work on network semantics is also of some relevance.

It was mentioned briefly in LtU here