Compositional Resource-Adaptive Certified System Software
Technical Report,01 Aug 2016,31 Aug 2018
Yale University New Haven United States
Pagination or Media Count:
The BRASS program aims to build resource adaptive systems that can operate under widely differing environments. This seedling project addressed several important technical challenges for building long-lived resource adaptive system software. CertiKOS layers were extended with formal resource models. New thread objects were added as basic building blocks and used to model the hardware and virtual device layers. A general mechanism for managing available CPU resources and support compositional layered refinement for concurrent programs on both single core and multicore machines was provided. A fully verified preemptive OS kernel with temporal and spatial isolation was developed.
- Computer Programming and Software