Interface Automata tooling for reasoning about shared-memory systems

A practical interface theory for concurrent components

When concurrent components communicate through shared memory, correctness is not only a question of whether each component works in isolation. It is also a question of whether their assumptions agree: which actions can occur, what data state an operation expects, and what state another component guarantees after it runs.

The IA Toolset is an open-source prototype for making those agreements explicit. It implements tooling around Interface Automata for Shared Memory (IAM), an interface theory for specifying and checking component compatibility when activities are triggered by synchronizing actions and data is communicated through shared variables.

The work grew out of the paper Interface Automata for Shared Memory, by Schinko, Vogler, Gareis, Nguyen, and Luettgen, published in Acta Informatica in 2022. Tri Nguyen is a co-author of the paper and a lead contributor to the toolset.

The problem: compatible parts are not enough

Interface Automata (IA) model a component as a labelled transition system whose actions are inputs, outputs, or internal transitions. An output initiates a synchronization and must be consumed by a corresponding input. If no matching input is available, the composition reaches a communication error.

This gives engineers a precise way to ask whether two components can work together. It also exposes an important property of concurrent software: a component may be locally valid while its interaction with another component is not.

Shared memory adds another layer. Two components can synchronize on the same action and still disagree about the data state that follows. An output may assume that an operation produces a state satisfying one condition, while the matching input guarantees a different one. The disagreement is an incompatibility at the interface boundary, even if the control flow looks correct.

The toolset makes these failures inspectable before they become failures in a closed system. Engineers can compose interface models, find communication errors, trace how an error state was reached, and check whether a more concrete component refines an abstract specification.

IAM: data at the boundary, without hiding the model

IAM extends the original IA setting with pre- and post-conditions attached to transitions. The conditions are predicates over algebraic expressions on shared variables.

• A pre-condition acts as a guard: it describes when the transition is enabled.
• The post-condition of an output transition is an assumption about the data state after synchronization.
• The post-condition of the matching input transition is a guarantee describing how the operation changes the shared state.

This separates two responsibilities cleanly. The output transition invokes or requests an operation and states what result it expects. The input transition describes the state change performed when that operation is handled. A communication error occurs either because the matching input is missing, as in IA, or because the input’s guarantee does not satisfy the output’s assumption.

The extension is deliberately conservative. IAM can be embedded into IA, and the embedding preserves the relevant composition and refinement behaviour. That matters in practice: adding shared-memory data does not require replacing the underlying compatibility concept with a less familiar one.

It also provides a useful finite abstraction. IAM can reason about infinite data domains without necessarily expanding every data value into a separate control state. The paper further gives a ground semantics for data-closed systems, where data states are made explicit, and shows that the reduced IAM structure is bisimilar to that ground semantics under the stated restrictions. In other words, the compact interface model remains connected to the standard closed-system treatment of data rather than being only a notation for assumptions.

From model to engineer’s workflow

The IA Toolset turns the theory into a small, usable modelling environment. Its textual language defines actions, shared variables, types, process templates, initialisation, products, compositions, and refinement checks. Interface behaviour is expressed with guarded commands and familiar control structures, including sequential composition, while loops, case statements, and goto labels.

Conditions sit close to the action they constrain. Guards appear before an action. Output post-conditions use assume; input post-conditions use guarantee. If a condition is omitted, it defaults to true. The language also distinguishes primed and unprimed variables in post-conditions, allowing a specification to refer to both the previous and resulting data state. That makes statements such as preserving a value or changing it by a defined operation explicit.

The toolset supports three complementary ways of working:

1. Compose and debug. Product construction reveals incompatible synchronizations and data assumptions. The debugger shows the relevant transitions and the action sequence that leads from the initial product state to an error.
2. Check refinement automatically. IAM refinement, expressed as alternating simulation, is reduced to a Boolean equation system. The prototype uses the mCRL2 toolset to solve that system.
3. Explore a failed refinement. Refinement also has a two-player game characterization. An engineer can select a move on the specification side, inspect matching transition families on the implementation side, and continue the game to understand why the relation does or does not hold.

The environment includes a textual editor with syntax highlighting and completion, a compiler-like interpreter for transforming the language into IAM automata, a simulator, a debugger, and a VS Code extension. The implementation is approximately 12,000 lines of code across its Kotlin backend, language front-end, and editor integration.

What this changes in engineering practice

Interface theories bring a useful discipline to component-based software. Instead of documenting integration assumptions only in prose or discovering them through end-to-end failures, a team can state what a component accepts, what it produces, and what must be true when components synchronize.

For shared-memory systems, the benefit is especially concrete. Data constraints become part of the interaction contract. Compatibility can be considered before deployment. Refinement provides a way to replace an abstract component with a more concrete implementation while checking that the implementation offers no fewer inputs and no more outputs than the specification permits.

This does not replace testing. It gives testing and implementation a more precise boundary: the model identifies incompatible behaviours and assumptions early, while the running system still has to validate performance, integration details, operational conditions, and the correctness of the implementation itself.

An honest boundary around the project

IA Toolset is a prototype, not a production-grade verification platform and not a claim that every concurrent system can be modelled economically. The project was built to demonstrate that IAM can be supported with practical tools and to explore small examples such as the vending-machine model described in the paper. Its authors do not claim that it scales to real-world concurrent systems as it stands.

That limitation is part of the evidence, not a footnote to hide. The project connects formal interface theory, a real modelling language, automated checking, debugging, and interactive counterexample exploration in one open-source codebase. It shows what a serious language-engineering approach to concurrent software can look like before productisation questions such as scale, usability across teams, and integration with existing development systems are solved.

Paper and source

The formal account is Interface Automata for Shared Memory, Schinko, Vogler, Gareis, Nguyen, and Luettgen, Acta Informatica, 2022.

• IA Toolset on GitHub — IAM modelling, composition, simulation, debugging, and refinement tooling.
• BahnDSL on GitHub — related open-source work in domain-specific language design and model-driven tooling.

IA Toolset is released as MIT-licensed open source. These projects are academic and personal research evidence of capability, not commercial client work.