Haha, yeah I was expecting no one would understand my request. The troubles of being short and concise. I also forgot to include the links I had prepared. :(
So as a short explanation, communicating sequential processes is a model developed by Tony Hoare in 1978 which is sort of like state machines, but well different.[3] One book about protocol design I have open right now is from Robin Sharp "Principles of Protocol Design" (2008) implies that CSPs have "gained prominence within recent years" because basically FSMs suck for parallel operations. Again, I want to use GSL to start off both the protocol and my codebase using state machines (so big thanks for the links Pieter and Kevin!). But if it'll be possible to generate a CSP style protocol using GSL from my state machine, I'd be enormously happy. Thus my questions: Did anyone ever try something like this remotely? Best, alex. P.S. The links: [1]: http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/ [2]: https://www.cs.ox.ac.uk/projects/fdr/ [3]: https://en.wikipedia.org/wiki/Communicating_sequential_processes On 14.04.2016 11:37, Pieter Hintjens wrote: > I don't understand half of what you're asking :) But in any case do > take a look at the tiny FSM / C code generator > (https://github.com/imatix/gsl/blob/b0aa393a6d00df2859f21aab0ccf6f203e18db96/examples/fsm_c.gsl) > that I've used happily in a few projects already. > > On Thu, Apr 14, 2016 at 11:30 AM, alex. <thissid...@riseup.net> wrote: >> 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 >> zeromq-dev@lists.zeromq.org >> http://lists.zeromq.org/mailman/listinfo/zeromq-dev > _______________________________________________ > zeromq-dev mailing list > zeromq-dev@lists.zeromq.org > http://lists.zeromq.org/mailman/listinfo/zeromq-dev > _______________________________________________ zeromq-dev mailing list zeromq-dev@lists.zeromq.org http://lists.zeromq.org/mailman/listinfo/zeromq-dev
