Compositional Resource-Adaptive Certified System Software
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 2018
- Accession Number
- AD1065014
Entities
People
- Zhong Shao
Organizations
- Yale University