Refinement rules for real-time multi-tasking programs
Colin Fidge · 1997
. We present several formal program refinement rules for designing multi-tasking programs with hard real-time constraints. 1 Introduction Practical theories of real-time task schedulability are now available, and are being supported by modern programming languages such as Ada 95. Nevertheless, methods for developing real-time multi-tasking programs, while well understood, still lack the degree of formality demanded by safety-critical applications. Here we present a set of formal refinement rules for designing real-time multitasking programs. The rules introduce the computational components assumed by real-time scheduling theory, and can thus exploit a known schedulability test. 2 Real-time multi-tasking refinement rules The rules are expressed using timed refinement calculus notation [14]. See Appendices A to C for the definitions used below. For brevity, the rules assume a single input and a single output, both of type integer. Generalisations to multiple variables and other type...