On Thu, 7 Mar 2019 at 14:14, Kaushik Chakraborty
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.
I'm interested in that part of the system as well. For what it's worth I was envisaging explicitly modelling each external process/component that could experience faults so that I could enumerate those failure states, and all combinations of them, exhaustively. I've also given passing thought to modelling faults within the internal processes so I could see what happens when dealing with Byzantine failures. Definitely something I should read up on.