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.
3rd International Symposium of Formal Methods Europe, Oxford, United Kingdom 18-22 March 1996
FME'96: Industrial Benefit and Advances in Formal Methods / Gaudel, M C, Woodcock, J (eds): pp.327-346