Integrating real-time scheduling theory and program refinement

We show how real-time schedulability tests and program refinement rules can be integrated to create a formal development method of practical use to real-time programmers. A computational model for representing task scheduling is developed within a 'timed’ refinement calculus. Proven multi-tasking schedulability tests then become available as feasibility checks during system refinement