Abstract

Autonomous systems, such as self-driving cars and drones, have become a part of our daily lives. Since these systems operate in and interact with the physical world, their correctness depends on both functional and temporal aspects. However, the increasing complexity of modern computing hardware and software often leads to unpredictable timing behavior in these systems, making temporal properties particularly challenging to ensure. This dissertation proposes novel approaches to specify and enforce temporal properties based on a comprehensive empirical study of real-world issues. The first half of this dissertation presents an empirical study that dissects the timing issues. The dissection begins by re-visiting the fundamental sources of timing uncertainty – hardware performance interference. It systematically characterizes potential timing interference channels. Building on that, the study empirically examines how such timing uncertainty manifests at the software level and how developers address these issues. To this end, the study further collects and analyzes real-world bug case studies, summarizing the pitfalls and challenges developers face in achieving correct temporal properties. The second half of this dissertation brings solutions to the previously identified issues. A new concept, data-flow availability, is proposed for specifying timing constraints. Unlike traditional approaches that express timing constraints from a control-flow perspective (such as scheduling policy or locking protocols), DFA adopts a data-flow perspective, enabling more expressive and precise specification of timing requirements. To demonstrate the practicality of DFA, this dissertation also presents a proof-of-concept system named Kairos. In addition to supporting the core features of DFA, Kairos incorporates a scheduling mechanism that ensures consistency in scheduling decisions across system layers. Finally, the dissertation extends the assurance of temporal properties to adversarial scenarios by introducing a novel recovery scheme. This scheme enables systems to regain availability even when software components are compromised.

Degree

Doctor of Philosophy (PhD)

Author's Department

Computer Science & Engineering

Author's School

McKelvey School of Engineering

Document Type

Dissertation

Date of Award

5-9-2025

Language

English (en)

Share

COinS