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'