Home » forums » LtU Forum

Protocol languages

I've begun to get interested in a language-based approach to network protocol development. There are some nice ones like Prolac and older ones like Estelle.

I'm systematically boiling down an RFC to an implementation, assuming such a thing is possible, and am looking for all approaches. I'm less interested in formal verification techniques that don't result in a usable piece of software, but all pointers are appreciated. I'd like to hear your experience with such techniques too. I'm looking at whatever google and citeseer spit out for "protocol languages" and "protocol compilers".

By Sriram Srinivasan at 2005-02-04 15:44 | LtU Forum | previous forum topic | next forum topic | other blogs | 7722 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Try Holzmann's Spin

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

By shm at Wed, 2005-02-09 07:10 | login or register to post comments

Dynamic temporal logic

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.

By Charles A Stewart at Wed, 2005-02-09 11:22 | login or register to post comments

sscop

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.

By yuri at Sat, 2005-02-19 01:12 | login or register to post comments

Network Semantics

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

It was mentioned briefly in LtU here

By Sriram Srinivasan at Thu, 2005-02-24 16:09 | login or register to post comments