Interfaces with a Behavioral Contract: Protocol State Machines in Practice

Many hard-to-find integration errors share the same root cause: misunderstandings about the actually allowed order of events on the interfaces between components, subsystems, or organizations. This dynamic behavior is usually described only in the accompanying documentation, as plain text or sequence diagrams. Both have significant drawbacks: plain text cannot be evaluated by tools, and sequence diagrams show only single examples of allowed or prohibited behavior. This article presents a methodology which makes dynamic behavior a formal part of the interface contract: the specification of protocol state machines.

Interfaces and IDLs: indispensable, but static

In any kind of software architecture, interfaces between components, subsystems or systems are important artifacts. They represent the contract not only between these architecture building blocks, but also between organizational units like teams, departments, or companies. Therefore, interfaces are often modeled as first-class entities using an Interface Definition Language (short: IDL). Compared to interfaces defined using a general-purpose programming language, IDL models are technology-neutral: the same definition can be mapped to a RESTful service or used to generate C++ code for an embedded system.

The landscape of IDLs has broadened considerably since the 2010s. For service-to-service communication, Protocol Buffers with gRPC dominates today; REST APIs are described with OpenAPI, event-based systems with AsyncAPI. In addition, design languages like TypeSpec (Microsoft) and Smithy (AWS) have emerged which can generate several of these formats from a single definition.

What all of them have in common is their focus on the static aspects of an interface, i.e., data types, attributes, and operations. However, often there are constraints on the order of interactions on the interface. E.g., an init() method has to be called before any other interaction is allowed. None of the IDLs mentioned above can express this property; even AsyncAPI only describes which messages exist, not their allowed order.

The method: behavioral contracts with protocol state machines

Contract-based interface development extends the contract by a behavioral dimension: a protocol state machine (short: PSM) is defined for each interface. It defines exactly what order of events is allowed on any implementation of this interface. Every sequence which is not covered by the PSM violates the contract. The concept originates from UML, where protocol state machines have long been part of the standard; in practice, however, they are rarely used there.

A formally defined PSM can be evaluated by tools. This results in several usage scenarios:

• Static checking: Implementations and clients can be verified against the PSM, e.g., by model checking. Protocol violations are detected before integration.
• Runtime monitoring: A monitor can be generated from the PSM which immediately reports contract violations in the running system.
• Trace validation: Messages recorded from a real-world system are checked against the PSM after the fact. As the messages exchanged between components can often be traced without changing the actual source code (e.g., by activating a probe in the communication infrastructure), this is a lightweight but powerful way to validate the dynamic interactions.
• Test generation: Mock servers and test clients can be generated from the interface definition and its PSM, allowing an interface to be tried out instantly.

Defining PSMs does mean additional effort; in our experience, however, an integration error found late costs considerably more.

Example: a music player interface with Franca IDL

How this methodology can be implemented in an IDL is shown by Franca IDL, one of the few IDLs which support protocol state machines as an integral part of the language. Franca was initiated in 2011 by the author of this article at the GENIVI Alliance (now COVESA) to standardize interfaces for in-vehicle infotainment platforms. The Eclipse-based core project is no longer actively developed; however, the CommonAPI C++ code generator built on top of it is still in use by car manufacturers and suppliers.

The following screenshot shows an example interface using Franca IDL. It specifies a simple music playback API.

The method findTrackByTitle selects a musical track based on an input string. From all matching tracks, the best match is set as attribute currentTrack; if no track can be found, the server returns a NOT_FOUND error code. After a track has been selected, the methods play and pause control the playback. All details about data types and interfaces of Franca IDL can be found in the reference chapter of the Franca User Guide.

The following PSM specifies the dynamic behavior for this interface. E.g., it defines that play can only be called after a successful call to findTrackByTitle. The initial state is Idle. Note that each Franca method is represented as a call/respond pair of transitions in the PSM.

In Franca IDL, the PSMs are written in textual form directly next to the interface definition. This makes the behavioral contract part of the same artifact as data types and methods, and it can be evaluated by all tools of the toolchain. Such a tool integration between Franca IDL and itemis CREATE is described in the blog post “State Machine Origami”. There, the communication of behavioral state machines is checked by means of Franca PSMs.

The methodology today: three representatives

Even though the mainstream IDLs still do not support behavioral contracts, the methodology itself is alive. Three representatives show this:

• Dezyne: The Dezyne language by Verum (open source since 2021) specifies interfaces with behavioral contracts as state machines and verifies components by model checking. Protocol violations are thus ruled out statically instead of being handled at runtime. The target group are embedded systems built by high-tech equipment manufacturers, for whom the cost of poor quality is high; Dezyne is in production use at Philips and ASML, among others. The ecosystem around the language has remained a niche, however.
• P: The P language, originally created at Microsoft and now developed further by AWS, models distributed systems as communicating state machines. AWS uses P for S3 and DynamoDB, among others; with the PObserve tool, production logs are validated against the formal specification after the fact — the trace validation described above, at large scale.
• Session types: Multiparty session types and the Scribble protocol language originate from research. A globally defined protocol is projected onto a finite state machine for each participant, from which monitors for the involved components can be generated. So far, the approach has mainly been used in research and pilot projects.

All three have in common that dynamic behavior is treated as a formal part of the interface contract and checked with tool support.

The effort barrier: drafting PSMs with AI support

So why has the methodology not been adopted more widely, despite its advantages? A major reason is the design effort. Designing a PSM for an interface requires thinking through the dynamic behavior completely; many developers perceive this as an additional burden on top of the actual implementation. We received this feedback from practitioners again and again while working on Franca in the GENIVI environment between 2011 and 2017.

Today, there is a new approach to this problem: capable AI agents. An agent can analyze the existing implementations of some clients and servers and derive a first draft of the PSM from them. If recorded trace logs are available as well, the draft can be checked against the actually observed behavior. The developer then reviews and refines the proposal; the responsibility for the contract remains with the developer.

This combination is attractive because both sides complement each other: the AI agent quickly delivers a draft, and the formal nature of the PSM ensures that this draft remains verifiable by tools. Errors made by the agent therefore do not go unnoticed, but become visible through model checking or trace validation. This considerably lowers the entry barrier for the contract-based methodology.

How one would build it today

Franca is closely tied to the Eclipse platform, whose adoption has declined considerably in recent years. If an IDL with protocol state machines were built today, the technical foundation would look different: with the Language Server Protocol (short: LSP), the language support can be implemented once and then used in VS Code, in the browser, or in other editors. Frameworks like Langium (the Xtext successor based on TypeScript) reduce the effort for this considerably. Checking traces against PSMs would be integrated into the CI pipeline, so that contract violations are detected automatically with every test run.

At itemis, we develop such tailor-made languages and tools in customer projects. The methodology of behavioral contracts can be integrated into modern toolchains just as well as Franca once demonstrated within Eclipse.

Conclusion

Tools age, methods do not. Franca IDL has shown that protocol state machines can be integrated seamlessly into an IDL; Dezyne and P show that the contract-based methodology is more relevant today than ever. Formally specifying the allowed order of events on an interface helps to find integration errors earlier and, at the same time, yields precise, tool-processable documentation of the behavior. The choice of the concrete technology is secondary; what matters is that the contract covers more than data types and signatures.

Custom Tools at itemis — We build tailor-made tools and integrations for your software development toolchain: Custom Tools →