Specifying functional and timing behavior for real-time applications

Abstract

We present a notation and a methodology for specifying the functional and timing behavior of real-time applications for a heterogeneous machine. In our methodology we build upon well-defined, though isolated, pieces of previous work: Larch and Real Time Logic. In our notation, we strive to keep separate the functional specification from the timing specification so that a task's functionality can be understood independently of its timing behavior. We show that while there is a clean separation of concerns between these two specifications, the semantics of both pieces as well as their combination are simple.