# Using Timing\_Event in SPARK to detect missed task deadlines

**URL:** <https://forum.ada-lang.io/t/using-timing-event-in-spark-to-detect-missed-task-deadlines/4749>\
**Category:** General\
**Tags:** spark, ada, gnat\
**Created:** [September 17, 2026, 9:24am UTC](https://forum.ada-lang.io/t/using-timing-event-in-spark-to-detect-missed-task-deadlines/4749 "2026-09-17T09:24:03Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![lorislibralato](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lorislibralato/32/1090_2.png) [@lorislibralato](https://forum.ada-lang.io/u/lorislibralato)\
**Post date:** [September 17, 2026, 9:24am UTC](https://forum.ada-lang.io/t/using-timing-event-in-spark-to-detect-missed-task-deadlines/4749/1 "2026-09-17T09:24:04Z")

</div>

I am trying to use `Timing_Event` to detect missed task deadlines.

At the Stone SPARK proof level, I get the following error when calling the `Set_Handler` procedure from `Ada.Real_Time.Timing_Events`:

`"Timing_Event_Handler" is not allowed in SPARK (due to access to protected subprogram)`

Is the `Timing_Event` interface incompatible with SPARK? Are there alternative ways to implement task deadline-miss detection in SPARK?

---

<div class="post-metadata">

**Author:** ![damaki](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/d/3bc359/32.png) [@damaki](https://forum.ada-lang.io/u/damaki)\
**Post date:** [September 17, 2026, 11:09am UTC](https://forum.ada-lang.io/t/using-timing-event-in-spark-to-detect-missed-task-deadlines/4749/2 "2026-09-17T11:09:41Z")

</div>

> [@lorislibralato](#):
>
> Is the `Timing_Event` interface incompatible with SPARK?

Yes, access to protected subprogram types are not currently supported by SPARK (they’re tricky since they could hide global effects). You could work around this by hiding the call to `Set_Handler` in another procedure whose body has `SPARK_Mode => Off`.

---

<div class="post-metadata">

**Author:** ![lorislibralato](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/lorislibralato/32/1090_2.png) [@lorislibralato](https://forum.ada-lang.io/u/lorislibralato)\
**Post date:** [September 17, 2026, 12:04pm UTC](https://forum.ada-lang.io/t/using-timing-event-in-spark-to-detect-missed-task-deadlines/4749/3 "2026-09-17T12:04:39Z")

</div>

Thanks for your answers