A sequential real-time refinement calculus |
| |
Authors: | Ian J Hayes Mark Utting |
| |
Affiliation: | (1) Department of Computer Science and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia (e-mail: ianh@csee.uq.edu.au) , AU;(2) Department of Computer Science, School of Computing and Mathematical Sciences, The University of Waikato, Private Bag 3105, Hamilton, New Zealand (e-mail: marku@cs.waikato.ac.nz) , NZ |
| |
Abstract: | We present a comprehensive refinement calculus for the development of sequential, real-time programs from real-time specifications.
A specification may include not only execution time limits, but also requirements on the behaviour of outputs over the duration
of the execution of the program. The approach allows refinement steps that separate timing constraints and functional requirements.
New rules are provided for handling timing constraints, but the refinement of components implementing functional requirements
is essentially the same as in the standard refinement calculus. The product of the refinement process is a program in the
target programming language extended with timing deadline directives. The extended language is a machine-independent, real-time
programming language. To provide valid machine code for a particular model of machine, the machine code produced by a compiler
must be analysed to guarantee that it meets the specified timing deadlines.
Received: 27 September 1997 / 13 June 2000 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|