‹Programming› 2027
Mon 15 - Fri 19 March 2027 Kyoto, Japan

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.