Chorer

What is Chorer?

Chorer is an analysis tool that examines Erlang programs and extracts formal models of their communication behaviour. Its purpose is to help developers uncover communication bugs in distributed and actor-based systems by using insights from Choreography Automata.

Choreography Automata¹

A Choreography Automaton is a labelled transition system that represents the communication behaviour of concurrent systems. Each transition is annotated with a communication action (such as sending or receiving messages), and the automaton describes all possible evolutions of the system.

Formally, the concept was introduced to model structured interactions and communication protocols in message-passing programs. Choreography Automata provide a foundation for verification, analysis, and reasoning on distributed systems.

Local View

A Local View denotes the behaviour of a single function within the program. It focuses on the transitions that originate from that function, describing the messages it sends and receives along with possible internal evolutions.

Global View

The Global View represents the entire behaviour of a system in a single automaton. Its transitions describe communication actions across all processes. This gives an overview of the complete behaviour of the program.

How does it work?

Chorer reconstructs the possible message-passing interactions between Erlang processes and represents them using Local Views and a Global View. The extraction follows a bottom-up, over-approximating approach: any communication that might occur is included. This ensures that potential issues, including subtle concurrency bugs, are highlighted without being missed. Deadlocks are highlighted directly in the Global View graph: they appear as red states. This web interface always uses the lastest version of Chorer.

⚠ This tool is an early prototype and still under active development, bugs, incomplete features, and unexpected behaviors are to be expected.

Extraction steps

1. The input file is parsed and basic syntactic and structural checks are performed. Chorer identifies processes, calls, and communication constructs.
2. For each discovered actor, the tool extracts a Local View, describing the behavior of that actor in isolation, including its possible send/receive actions.
3. All Local Views are combined into a Global View, reconstructing the inter-process communication structure of the whole system.
4. The generated automata can be minimized and further analyzed to detect inconsistent communication patterns or potential concurrency bugs.

For a deeper explanation of the ideas behind Chorer, including its theoretical foundations, strengths, and limitations, please refer to the accompanying thesis² (outdated, only in italian), paper³ and poster.

References

1. Barbanera, Franco, Ivan Lanese, and Emilio Tuosto. "Choreography automata." International Conference on Coordination Languages and Models. Cham: Springer International Publishing, 2020 (COORDINATION).
2. Genovese, Gabriele. "ChorEr: un analizzatore statico per generare Automi Coreografici da codice sorgente Erlang." (2023).
3. Genovese, Gabriele, Ivan Lanese, Cinzia Di Giusto, Emilio Tuosto, and Germán Vidal. "Choreographies for Program Understanding." International Conference on Formal Techniques for Distributed Objects, Components, and Systems. Cham: Springer Nature Switzerland, 2025 (FORTE).