Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation
Abstract
The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (e.g., loss of lives or failure of a mission). Such properties require strong isolation between components and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of the concrete implementation of the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 20, 2019
- Source ID
- 10.1145/3371088
Entities
People
- David Costanzo
- Jung-Eun Kim
- Lionel Rieg
- Man-Ki Yoon
- Mengqi Liu
- Ronghui Gu
- Zhong Shao
Organizations
- Columbia University
- Defense Advanced Research Projects Agency
- Grenoble Alpes University
- National Science Foundation
- Yale University