Admin: 1 revision

2011-12-12T10:06:27Z

1 revision

New page

[[Category:WG211]]

<h1>Timing Verification of Hume Box Compositions
via Abstractions in Agda2</h1>
<h3>Christoph Herrmann</h3>

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.

WG211/M7Hermann - Revision history

Admin: 1 revision