WG211/M7Hermann

Timing Verification of Hume Box Compositions via Abstractions in Agda2

Christoph Herrmann

Hume is a language developed for functional programming of safety-critical, real-time systems. In Hume, programmable boxes are wired to a network with potential cycles. We are interested in verification of reaction time from an input event to the corresponding output event. This can involve repeated executions of boxes. The analysis for single Hume boxes has already reached a high degree of maturity, but there is still need for a precise verification of box compositions. In our current research we model Hume boxes by functions in the dependently typed language Agda2. The original box implementations are abstracted to the properties of interest, and enriched with timing information gained from single box analysis. Distinguished program values which decide about consumption/production of box I/O data, selection of branches within a box and number of box iterations are reflected in the Agda2 types, as well as quantitative timing information. Timing constraints in the type decide whether the type of the function which expresses the composition can be constructed. The Agda2 type checker accepts the composition, if and only if the composition satisfies the specified constraints.