2011/12/21 by Brijesh Dongol, Ian J. Hayes, Dongol, Brijesh +1
Computer Science · #Embedded Systems Design Techniques #Formal Methods in Verification #Real-Time Systems Scheduling
paper · doi:10.14279/tuj.eceasst.46.684.701
openalex publication_date 2011/12/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/15
Abstract: Timed specifications are often formalised at an absolute level of pre-cision, which does not reflect the real world that the specifications model, i.e., in the real world, inputs cannot be sampled with absolute precision and physical hard-ware cannot react instantaneously. As a result the developed specifications can often become unimplementable. In this paper, we consider the time bands model which allows time to be structured into several layers of abstraction and relationships be-tween bands to be formalised. This allows the timed specifications developed under idealised assumptions to be approximated using the time band in which the variables are sampled. We implement the approximated specifications using teleo-reactive programs embedded with time bands.