The deadline command

The deadline command is a simple, yet highly flexible, language primitive for real-time programming. Formally, it has a straightforward definition as a constraint on the current time. In practice, it acts as a compiler directive, which can be checked statically, to ensure that the program will always meet its timing requirements. As a concrete example, a way of adding the deadline command to the safety-critical SPARK programming language is described. A detailed comparison is made with other proposed real-time language constructs