Formal description of a real-time operating system using RTPA

Most industrial computing systems are real-time systems where rigid time constraints must be met. Great attention should therefore be given to the design of real-time operating system (RTOS) because its malfunction may result in a disaster both to business and human life. Current RTOS´s are target-machine and application specific. This paper develops a new architecture of RTOS´s, RTOS+, which is generic and portable to different platforms. We adopt real-time process algebra (RTPA) to specify and describe RTOS+, particularly its architecture and dynamic behaviours. On the basis of the formal specification, architecture, behaviours, and correctness of RTOS+ can be guaranteed. The core operations of RTOS+, such as task scheduling, time, event and resource management can be rigorously described for better real-time performance and improved resource utilization.