详情

原文传递 Compositional Resource-Adaptive Certified System Software.

题名：	Compositional Resource-Adaptive Certified System Software.
作者：	Shao, Z.
关键词：	Operating systems, Computer program verification, System software, Central processing units, Adaptive systems, Device drivers, Software development, Kernels (operating system), Program verification, Formal methods, Resource-aware abstraction layers, Concurrency, Temporal and spatial isolation
摘要：	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.
报告类型：	科技报告