@inproceedings{dc55dd239eff4412ad58f1a62f6a88ff,
title = "Formal Development of a Real-Time Operating System Memory Manager",
abstract = "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.",
keywords = "Event-B, Memory Manager, Operating System, refinements",
author = "Wen Su and Abrial, \{Jean Raymond\} and Geguang Pu and Bin Fang",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015 ; Conference date: 09-12-2015 Through 11-12-2015",
year = "2016",
month = jan,
day = "15",
doi = "10.1109/ICECCS.2015.24",
language = "英语",
series = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "139",
booktitle = "Proceedings - 2015 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015",
address = "美国",
}