Safety critical systems, such as aviation systems controlled by software, often have hard real-time requirements. Producing the correct resultat the right time is thefundamental goal of such systems. Formally specifying the system functions and the timing requirementsis the crucial step towards achieving such a goal. Aviation systems often need to be modijied or upgraded on a regular basis, i.e.functionality and timing constraints may be altered. Therefore, theformal specijication of such systems needs to be easily reused, maintained and modijied. Thispaper demonstrates how the task scheduling aspects of an aircraft mission computer can beformalised in TCOZ.
Jin Song Dong, Brendan P. Mahony, Neale Fulton