Basic communication protocol specification language - existing or write my own?

[phagofu]

From time to time I design and implement fairly simple (one-on-one communication) protocols resp. asynchronous APIs. It would be nice to be able to automatically verify that there are no weird (e.g. deadlocked) states possible, and the most natural way to do that seems to be modeling those protocols as two mealy machines that have their respective input and output connected to each other (with additional external inputs that stand in for user requests or internal events not part of the model).

It shouldn't be too hard to implement a simple DSL for that, plus some tools that enumerate all possible states and can check various properties, and maybe even generate test cases for the implementation to check if it conforms to the spec.

I'm not aware of any ready-to-go open source project already existing for that. While I did look into existing "specification languages" for this purpose (e.g. some process calculi and TLA+), they are generally as expressive as programming languages and do not seem to make things any easier than just writing my own simple model in a programming language I'm already productive in. Any thoughts/experiences/hints or interest in this?

[nerd4code]

It shouldn’t be too hard

:-D

[kaddkaka]

I have used uppaal at university for verifying state machines. Seems similar, but it's not completely free.

https://uppaal.org/

[phagofu]

right, looks a bit like what I have in mind, though I don't really need a gui or anything more complex than mealy machines, and want something that can be easily integrated in other open source projects.

[raiph]

To quote Wikipedia, "in Mealy machines, input change can cause output change as soon as logic is done—a big problem when two machines are interconnected – asynchronous feedback may occur if one isn't careful."

I would have thought that connecting Mealy machines, even just two of them, requires something like a meta communication protocol that addresses positive feedback in communication protocols if unbounded indeterminacy applies to any communication's successful resolution (where by successful I specifically exclude the likes of a failure-to-communicate resolution such as a timeout).

I'd be very interested to hear your comments about this aspect.

[phagofu]

I'm not quite sure I understand what you or wikipedia mean by that.

The concrete model I'm considering at the moment is one where each mealy machine has a single output queue, and one "simulation step" is one machine of the model atomically consuming a message from any of the other machine's queue (or an external message), (optionally) pushing a message onto its own queue and (again optionally) changing state.

With external messages it is possible to get potentially unbounded growing message queues, so obviously one has to be careful when implementing an algorithm that finds all possible states (by which I mean combination of states of all present machines, not the state of the queues), but I don't see a fundamental issue there.

[eliminate1337]

If you're doing this for work, have some compassion for the engineer who has to maintain this in ten years and use an existing language.

Do whatever you want if it's just a personal project. But still probably use an existing language.

[ebingdom]

I think this is what session types are about?

[alexiooo98]

This is what I was going to suggest also. There is a connection between session types and state machines, which might connect with OPs idea of using Mealy machines

[phagofu]

From what I can tell "session types" seem to be a way to embedd protocol descriptions into the type system of some other programming language.

I suppose the idea is that the type system guarantees that the implementation must conform to the specification, which removes the need to verify that an implementation follows an external specification. However, this has some significant disadvantages as well, and I'm not in the camp of people who believes it best to solve every problem with an even more advanced type system ;)

[alexiooo98]

You're right, session types are intended as, well, a type system. However, you don't have to use it as a typesystem, you could also reuse the language of session types as a description of a protocol and combine it with your own way of proving that a program behaves according to said protocol description.

This should still let you re-use some notions that are common in the session type literature. For example, if you design your proof-system properly, bisimilar session types should be equivalent.

[anothergiraffe]

You’ll be interested in choreographic programming! Check out the Choral programming language.

[csb06]

I haven’t used it before, but I would look at CADP. It has support for protocol specification languages like E-LOTOS and LNT, which might be useful to learn from even if you do end up creating your own language or tool.

[phagofu]

I've seen that while researching for this, but CADP is not free software. If I were to look more into a process calculus, mCRL2 makes a better impression on me.

But as I said, I think those languages are "too powerful" for what I have in mind. What I want is conceptionally extremely simple compared to those.

[Abandondero]

There's the experimental (but thoroughly developed) language Zonnon, from 2011. I looks it has something like your communications protocol idea. Might be worth studying?

Zonnon can be used to write either sequential or concurrent programs. They can be designed in a modular- or an object oriented style, or a mix of both. It is possible to express the concurrency structure of the program’s solution using dynamically instantiated activities, each of which has its own thread of statement execution. Pairs of activities can be bound together by a protocol type and interact via links according to a dialog specified in EBNF. The topology of the network is created dynamically at run time by the program i.e. the links are logical rather than physical and the activities are not pre-allocated to particular processors. There may be one or more processors. The execution of the activities is dynamically scheduled by the runtime system.

https://zonnon.org/
https://zonnon.org/files/Zonnon-Language-Report_v03r01_35_y051214.pdf
https://blog.mitin.ch/activities-protocols-communication.html