[Haskell-cafe] Informal modelling and simulation of protocols

[MarLinn]

2cents:

AFAIK in existing general-purpose simulation frameworks the type of
simulation you need for this type of problem is typically implemented in
a way that very closely resembles "classical" FRP, particularly it's
definition of events. The framework basically manages huge queues of
time-action-pairs.

So several of the FRP libraries might be a good candidate. I haven't had
a chance to experiment with MSF's yet, but seeing as they are a
development in FRP space, Ivan's approach sounds like quite a good idea.

Cheers.

On 05/03/2019 14.29, 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