ABSTRACT
This chapter presents a set of guidelines for modeling operating system (OS) kernels for embedded real-time systems in Event-B. It provides a set of modeling guidelines of real-time operating systems (RTOSs), including scheduling and context switch, interrupts, queue management, and memory management. The guidelines focus on the basic functionality of RTOS and represent the primary requirements of RTOS for an Event-B model. RTOS is a class of operating systems that is used for applications that have time constraints. The chapter describes some of the basic features and concepts of four RTOSs: FreeRTOS, UCOS, eCos, and VxWorks. In real-time kernels, each process has a priority as defined in the process block. Queues are the primary object of process–process communications. The RTOS provides memory management techniques to assign memory to objects. The main components of a FreeRTOS are task, queue, and memory.
