Coconut: Typestates for Embedded Systems

Typestate programming defines object states and actions to improve software safety by ensuring operations on objects follow the correct sequence. While its adoption in object-oriented languages has increased, limitations persist in the features supported. Typestates are particularly useful in embedded systems for operation sequencing, yet examples in this area are scarce. We introduce Coconut, a C++ tool that leverages typestate programming with templates for specifying typestates and combining static type checking and dynamic analysis to ensure proper class instance behaviour. It uniquely supports advanced programming features like branching, recursion, aliasing, concurrency, and optional typestate visualisation, facilitating idiomatic object-oriented programming with inheritance. Illustrating its effectiveness, we apply Coconut to actual embedded system projects, advancing the field by introducing a comprehensive set of features and practical examples for implementing typestate programming.