Nordic Journal of Computing 14(2008), 173–201. FORMALISING SCHEDULING THEORIES IN DURATION CALCULUS

Abstract. Traditionally many proofs in real time scheduling theory were informal and lacked the rigor usually required for good mathematical proofs. Some attempts have been made towards making the proofs more reliable, including using formal logics to specify scheduling algorithms and verify their properties. In particular, Duration Calculus, a real time interval temporal logic, has been used since timing requirements in scheduling can be naturally associated with intervals. This paper aims to improve the work in this area and give a summary. Static and dynamic priority scheduling algorithms are formalised in Duration Calculus and classical theorems for schedulability analysis are proven using the formal proof system of Duration Calculus. ACM CCS Categories and Subject Descriptors: X.X.X [not known yet