Dominik Katkó

Software Developer @ Trifork

Software Developer at Trifork, interested in functional programming, formal verification, cool architecture and unique problems. 

He implemented the Language Server Protocol in the Wrangler Erlang refactoring tool and now he is investigating how to bridge a gap between Elixir distributed systems and their formal models. 

He believes that the best solution starts on paper, and achieved in collaborative communities, where trust is key.

Model-based development and analysis of distributed systems with Elixir and mCRL2

Formal methods offer powerful techniques for analyzing complex distributed systems, yet their adoption in industry often faces significant barriers. Modelling real-world systems typically involves steep learning curves and high costs, while the automatic generation of formal specifications from existing industry code remains an ongoing challenge.

This talk presents a lightweight approach to developing distributed Elixir systems supported by formal specifications. We introduce a high-level domain-specific language that enables developers to define distributed protocols, which are then automatically translated into both an mCRL2 formal model and an Elixir implementation with identical behaviour.

We'll discuss key challenges in language design, formal model simulation, and ensuring implementation fidelity.

The talk will showcase case studies, including a simplified RAFT protocol, demonstrating how this approach enhances reliability and correctness in distributed system development.

←Back