From ideal to realisable real-time specifications
Gale Smith · 1999
. Formally refining a real-time specification to an implementation is only possible when the specification allows for all physical limitations, and timing and signal errors inherent in the implementation. Allowing for such implementation-specific details in a top-level specification can, however, obscure the desired functionality and complicate analysis. Furthermore, such an approach assumes the specifier has an understanding of the physical limitations and errors of the implementation which may not yet have been developed. As an alternative, we propose introducing a notion of realisation into the formal development process. Realisation is an approach to specification development which allows errors and physical limitations to be introduced. It also allows properties of the new specification to be derived from those proved for the original. 1 Introduction Several formal notations have been developed for the specification and refinement of real-time systems [19, 15, 16, 3, 13, 12]. To ...