TimedCoconut: Platform-Driven Typestates Extension for Embedded C++
Ensuring embedded systems satisfy both behavioural protocols and timing requirements on deployed hardware is challenging, particularly when such properties are analysed separately. This often leads developers to rely on late-stage profiling and testing, where timing violations may be discovered late in development or after deployment. We present TimedCoconut, a GCC-based verification toolchain that extends C++ behavioural protocols, i.e. typestates, with transition-level timing constraints. TimedCoconut enables programmers to specify both permitted sequences of operations and their temporal bounds directly at the type level. Verification proceeds in two compile-time phases. First, TimedCoconut checks operation ordering and potential logical timing problems against the declared timed typestate, independently of the target hardware. Second, it invokes the Bound-T WCET analysis tool to validate that the compiled program satisfies the declared timing bounds on the selected target platform. We evaluate TimedCoconut on five time-critical embedded applications running on two target platforms, ARM and AVR. The results show that measured execution times remain within the predicted WCET bounds, demonstrating that TimedCoconut provides safe over-approximations of execution time while enforcing both behavioural and timing constraints. This shifts timing validation from late-stage hardware testing to compile-time checking of timed typestate protocols against target-specific execution bounds.