Nikolaus Huber: Types and Time: Languages, Tools, and Methods for Reliable Systems Engineering

Abstract

Software plays a vital role across many areas of modern society. The personal gadgets we carry with us every day, the medical devices many people rely on, and the massive city-spanning systems that keep our critical infrastructure up and running are all powered by software, which is at the heart of every modern computing device. Naturally, we are therefore interested in ensuring that its execution is as error-free as possible, as errors might lead to significant financial loss or even endanger human life. To that end, this dissertation presents work aimed at helping design, implement, and verify reliable software systems.

The first part of this dissertation presents a design for a programming language for the development of embedded systems, called Mimosa. Mimosa builds upon MIMOS, a novel model of computation that allows for describing an overall software system as a graph of computation nodes. As this model enjoys both functional and timing determinism, Mimosa is particularly suited for the development of software for real-time systems. The presented work covers formal semantics, simulation, and compilation to a set of tasks running on a real-time operating system.

The second part of this dissertation presents broader work in the realm of reliable software engineering, targeting, in particular, software systems developed in the programming language OCaml. First, a tool for dynamic verification of stateful OCaml programs is presented. The primary focus of the tool lies on the automatic extraction of a functional model from formal contracts provided as part of a module's interface. Second, a method for encoding interaction nets, a particular form of graph rewriting, in OCaml is presented. Particular properties of interaction nets enable automatic scaling of the rewriting process across multiple processing cores. Compared to previous work, the presented encoding focuses on correctness guarantees provided by the interaction net type system, which is encoded in the type system of OCaml. It is shown that certain algorithms can exploit the inherent parallelism of the rewriting process, and therefore automatically utilise OCaml's recently added native support for parallel evaluation.