[Haskell-cafe] Informal modelling and simulation of protocols

Thu Mar 7 01:13:54 UTC 2019

Hi,

> - Model small sats as Monadic Stream Functions [1], implement a communication protocol on top (also using MSFs), and use quickcheck + fault injection to verify distributed consensus in the presence of faults. The next (immediate) step will be to bound the trace length and use smallcheck or something that exhausts the input space. I have also implemented Raft using MSFs, and the idea is to verify properties in a similar way.

I am interested to know the "fault injection" part. Did you inject the same randomly as in general Chaos Engg style or used formal techniques like LDFI (lineage driven fault injection
)? Is there some reference code that you can share. 
Thanks in advance. 

Cheers!
Kaushik
https://keybase.io/kaushikc/

On Tue, Mar 5, 2019, at 19:00, Ivan Perez wrote:
> Hi
> 
> Partly related; for recent work we did two things:
> 
> - Model part of the collision avoidance logic of a satellite as a state machine, implement it in haskell (14 locs) and use small check to verify that the state transitions fulfill the properties we expect for collision avoidance.
> 
> - Model small sats as Monadic Stream Functions [1], implement a communication protocol on top (also using MSFs), and use quickcheck + fault injection to verify distributed consensus in the presence of faults. The next (immediate) step will be to bound the trace length and use smallcheck or something that exhausts the input space. I have also implemented Raft using MSFs, and the idea is to verify properties in a similar way.
> 
> I know this is vague. Let me know if you have any questions or want more details.
> 
> Ivan
> 
> [1] https://github.com/ivanperez-keera/dunai
> [2] https://arc.aiaa.org/doi/abs/10.2514/6.2019-1187
> 
> On Mon, 4 Mar 2019 at 02:05, P Orrifolius <porrifolius at gmail.com> wrote:
>> 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.
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190306/17017d7d/attachment.html>