Using Timing_Event in SPARK to detect missed task deadlines

General
, ,
1

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?

2

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.

3

Thanks for your answers