First of all I wasn't really sure if it's okay to talk about the GSL Universal Code Generator on this list, but I am writing anyway since it didn't have its own mailing list. So forgive any insolence. :)
I was planning on writing my thesis about a traffic analysis resistant multi-user file-transfer protocol and sure enough I wanted to do the proof-of-concept implementation using ZeroMQ (so, yeah, expect to hear more from me over the next months ;) ). Now I haven't ever written a protocol myself but from the (little) research I did, I came to the conclusion that it would be best to formalize it as best as possible, in particular preventing any indeterminism. So the first idea was to use finite state machines for formalization and for some reason the best tool I could find for writing finite state machines that also lets me write test cases AND generate all kinds of code (including graphics and C-bindings) was made by the same people who created ZeroMQ. What about that, I thought to myself. Anyway after doing a little more research some papers indicated that a better approach for writing communication protocols would be communicating sequential processes (CSP). But they are somewhat of an antithesis to FSMs: their basic elements are processes whereas in FSMs the basic elements are states. Now I could brush CSPs aside and just go for FSMs, but since my thesis is mostly security/cryptography related, I also looked for security protocol analysers and every tool I could find was using CSPs as well. In particular I found Casper[1], which uses a special kind of CSP syntax to generate formalized CSP to be then checked with FDR3[2]. In short, the scenario I would love to go for is basically: - writing FSM in iMatix' GSL syntax, - compile it to Casper's CSP syntax, - compile that to general CSP to be checked by FDR3. My question to this fine community is thus: Did anyone ever try to produce a CSP using the GSL Universal Code Generator? Is something like that even achievable (without wasting large amounts of precious time) using GSL? Or in general, did anyone ever try to translate FSMs into CSPs? Or am I just too uninformed to know that something like this is simply absurd? All the best, alex. _______________________________________________ zeromq-dev mailing list [email protected] http://lists.zeromq.org/mailman/listinfo/zeromq-dev
