Formal Development of a Real-Time Operating System Memory Manager

This paper presents the formal development of the memory management module of a real time operating system. The interesting feature of this type of memory manager is that its dynamic memory allocation/reallocation mechanism behaves in O(1) (no loops). This brings a serious challenge on the "correct by construction" approach used to build this kind of system. This is due to the necessity to elaborate some delicate algorithms associated with complex data structures. To overcome this challenge, we follow the refinement principles of Event-B: we construct the proved executable code from some initial requirements. This development is interesting because some of the encountered problems are rather necessary to be studied in formal proved developments, among which are a modular encapsulation development, the design pattern of a linked list, and the usage of guarded events to develop pre-conditioned operations. It also gives us the opportunity to study a complex program construction in some general terms going beyond this specific example.