Chair: Jean-Baptiste Jeannin

Abstract:
Cyber-Physical Systems contain software components that interact with the physical world. Consequently, they are often found in aircraft, robots, or industrial processes where software failures have real, immediate, and potentially catastrophic consequences. These very interactions with the physical world also make them challenging to design safely because testing at runtime is often either impractical or incomplete. Alternatively, formal verification can statically derive rigorous safety guarantees, but the language in which CPS software is written determines both the ease of verification and its trustworthiness.

The first part of the dissertation presents a programming language addressing the trust gap that often exists between verification and execution. Formal verification requires accurately and reliably predicting program behavior through its semantics, but commonly used CPS languages typically have complex or imprecise semantics that make this difficult. However, languages and theories favoring verification are often not expressive enough to produce executable programs. Consequently, the software that is verified is often different from the software that executes. We present MARVeLus, a programming language and runtime that combines the expressive yet precise semantics of synchronous programming with efficient, modular verification via refinement type checking, to enable formally-verifiable, executable programs. We characterize the semantics of the underlying synchronous language, develop typing rules, and formally prove that verified specifications are maintained by the semantics. We then demonstrate real-time execution of verified programs on a robotics platform.

The second part details our generalization of quantitative semantics, which enables optimization-driven verification techniques to efficiently locate potentially unsafe behaviors or configurations of cyber-physical systems. Although many different quantitative semantics exist in the literature, they are often isolated in their own solver interfaces making them difficult to methodically compare with one another or verify for safety. We present the first generalized framework for quantitative semantics that is capable of instantiating and verifying the soundness of both existing and novel semantics. We formally prove the correctness of the generalization and use it to experimentally compare the performance of semantics.

Both MARVeLus and the quantitative semantics generalization strive to make formal verification more versatile, accessible, and dependable.