Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolation
Abstract
Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 31, 2022
- Source ID
- 10.1145/3563290
Entities
People
- Hao Chen
- Jung-Eun Kim
- Man-Ki Yoon
- Mengqi Liu
- Zhong Shao
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- Yale University