[Haskell-cafe] Informal modelling and simulation of protocols

[P Orrifolius]

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