[Haskell-cafe] Informal modelling and simulation of protocols

[Ian Denhardt]

This library may be of interest:

    https://hackage.haskell.org/package/dejafu

Quoting P Orrifolius (2019-03-04 02:05:06)
> Hi,
>
> this will probably be a somewhat rambling, open-ended question... my
> apologies in advance.
> There are some concrete questions after I explain what I'm trying to
> achieve, and some of them may even make sense!
>
> I'm planning on writing a multi-party, distributed protocol.  I would
> like to informally model the protocol itself and the environment it
> would run in and then simulate it to see if it achieves what I expect.
> Then it would need to be implemented and tested of course.
> I think a formal, mathematical model of the protocol would be beyond
> my abilities.
>
> I'm looking for any advice or tool/library recommendations I can get
> on the modelling and simulating part of the process and how that work
> could be leveraged in the implementation to reduce the work and help
> ensure correctness.
>
>
> I have some ideas of how this could work, but I don't know if I'm
> approaching it with a suitably Haskell-like mindset...
> What I envisage at the moment is defining the possible behaviour of
> each party, who are not homogeneous, as well as things which form the
> external environment of the parties but will impact their behaviour.
> By external things I mean, for example, communication links which may
> drop or reorder packets, storage devices which may lose or corrupt
> data, machines that freeze or slew their clock... that sort of thing.
> I'm also picturing a 'universal coordinator' that controls interaction
> of the parties/environment during simulation.
>
> Modelling each party and external as a Harel-like statechart seems
> plausible.  Perhaps some parts could be simpler FSMs, but I think many
> will be reasonably complex and involve internal state.
>
> It would be nice if the simulation could, to the limit of given
> processing time, exhaustively check the model rather than just
> randomly, as per quickcheck.
> If at each point the universal coordinator got a list of possible next
> states from each party/external it could simulate the
> simultaneity/sequencing of events by enumerating all combinations, of
> every size, of individual party/external transitions and then
> recursing with each separate combination applied as being the next set
> of simultaneous state transitions.
>
> To reduce the space to exhaustively search it would be nice if any
> values that the parties used, and were being tested by, were
> abstracted.  Not sure what the technical term is but I mean asserting
> relationships between variables in a given domain, rather than their
> actual value.
> For example, imagine a distributed vote between two nodes where each
> node must vote for a random integer greater than their last vote.
> Each node is a party in the protocol.
> In the current branch of the exhaustive search of the protocol a
> relation between node 1's existing vote, v1, and node 2's existing
> vote, v2, has already been asserted: v1>v2.
> So when the coordinator enumerates the possibilities for sets of
> next-state transitions, with each node n asserting vn'>vn in their
> individual party state transition, it will prune any search branch
> which doesn't satisfy the union of the assertions (v1>v2, v1'>v1,
> v2'>v2), and recurse into the search branch alternatives with v1'<v2',
> or v1'=v2', or v1'>v2'.
>
>
>
> So, some questions...
>
> Is what I'm suggesting even vaguely sensible way to approach the
> problem in Haskell?  Or am I getting carried away and some neat tricks
> zipping list monoids or something will get the job done?
>
> Is there some fantastic tool/library which already does everything I want?
>
> Are there any good tools or libraries in Haskell for defining and
> manipulating statecharts?
>
> The sessiontypes, and sessiontypes-distributed, libraries are cool,
> representing the protocol at the type level... but these only handle
> point-to-point, two-party protocols, right?
> I expect that extending them would be a _serious_ amount of work.
>
> Can quickcheck do the sort of exhaustive coverage testing that I'd like?
>
> Again, not sure of the correct terminology but can quickcheck generate
> tests at a variable-relation assertion level?  I.e. inspect the
> operators and boolean tests over a domain (+, ==, >=, append, length,
> contains, etc) and explore test cases according to whether certain
> relations between variables hold.
>
> Any feelings/opinions about whether Oleg Kiselyov's Typed Tagless
> Final Interpreter (http://okmij.org/ftp/tagless-final/index.html) work
> might be a useful mechanism to define the behaviour of parties within
> the protocol (the statecharts, basically) and then have different
> interpreters that enable both the testing  and implementation of the
> protocol, to keep them more closely aligned?
> I read that work years ago and have wanted to try it out ever since,
> so I may be overlooking the fact that it's totally unsuitable!
> Perhaps superseded now, but if it can allow more of the protocol to be
> expressed at the type level that would be good.
>
>
> Yeah, rambling.  Sorry about that.
>
>
> Thanks!
> porrifolius
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.