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. <[email protected]> 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 > [email protected] > http://lists.zeromq.org/mailman/listinfo/zeromq-dev _______________________________________________ zeromq-dev mailing list [email protected] http://lists.zeromq.org/mailman/listinfo/zeromq-dev
