A sequential real-time refinement calculus
A sequential real-time refinement calculus
复制标题
顺序实时细化演算
作者：
I. Hayes;M. Utting
抽象的。我们提出了一个全面的细化演算的发展顺序，实时程序的实时规范。规范不仅可以包括执行时间限制，还可以包括在程序执行期间对输出行为的要求。该方法允许细化步骤，分离的时间约束和功能要求。提供了新的规则来处理时间约束，但是实现功能需求的组件的细化本质上与标准细化演算相同。细化过程的产物是用定时截止期限指令扩展的目标编程语言的程序。扩展语言是一种独立于机器的实时编程语言。为了给特定型号的机器提供有效的机器码，必须分析编译器产生的机器码，以保证它满足指定的时间期限。
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.