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 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'.

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.

TLA plus might suit you! I've actually had some success going back and forth between copattern style code and TLA specs, its not easy and not perfect, but it works i've been slowly experimenting with modelling protocols as coinductive / copattern style trick https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating... is a small toy exposition i did i am messing around with some reusable abstractions, though its definitely a challenging problem On Mon, Mar 4, 2019 at 2:05 AM P Orrifolius 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'.

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.

This library may be of interest: https://hackage.haskell.org/package/dejafu Quoting P Orrifolius (2019-03-04 02:05:06)

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'.

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.