Doctoral Thesis Defense - Renato Jorge Araújo Neves

Friday, June 22, 2018, 10:00am

Title: Hybrid programs

Abstract: This thesis studies hybrid systems, an emerging family of devices that combine in their models digital computations and physical processes. They are very quickly becoming a main concern in software engineering, which is explained by the need to develop software products that closely interact with physical attributes of their environment e. g. velocity, time, energy, temperature – typical examples range from micro-sensors and pacemakers, to autonomous vehicles, transport infrastructures and district-wide electric grids. But even if already widespread, these systems entail different combinations of programs with physical processes, and this renders their development a challenging task, still largely unmet by the current programming practices. Our goal is to address this challenge at its core; we wish to isolate the basic interactions between discrete computations and physical processes, and bring forth the programming paradigm that naturally underlies them. In order to do so in a precise and clean way, we resort to monad theory, a well established categorical framework for developing program semantics systematically. We prove the existence of a monad that naturally encodes the aforementioned interactions, and use it to develop and examine the foundations of the paradigm alluded above, which we call hybrid programming: we show how to build, in a methodical way, different programming languages that accommodate amplifiers, differential equations, and discrete assignments – the basic ingredients of hybrid systems – we list all program operations available in the paradigm, introduce if-then-else constructs, abort operations, and different types of feedback. Hybrid systems bring several important aspects of control theory into computer science.

One of them is the notion of stability, which refers to a system’s capacity of avoiding significant changes in its output if small variations in its state or input occur. We introduce a notion of stability to hybrid programming, explore it, and show how to analyse hybrid programs with respect to it in a compositional manner. We also introduce hybrid programs with internal memory and show that they form the basis of a component-based software development discipline in hybrid programming. We develop their coalgebraic theory, namely languages, notions of behaviour, and bisimulation. In the process, we introduce new theoretical results on Coalgebra, including improvements of well-known results and proofs on the existence of suitable notions of behaviour for non-deterministic transition systems with infinite state spaces.

Supervisors: Luís Soares Barbosa and Manuel António Martins

Jury: - Rector of the University of Minho

        - Doctor Luís Manuel Dias Coelho Soares Barbosa (University of Minho)

        - Doctor Gabriel de Sousa Torcato David (University of Porto)

        - Doctor Marcello Bonsangue (Leiden Institute of Advanced Computer Science da Leiden University)

        - Doctor Tarmo Uustalu (Reykjavik Universiry)

        - Doctor Ernst-Erich Doberkat (Fakultät für Informatik da Technische Universität Dortmund)

Location: Auditorium B2 - Campus de Gualtar - Universidade do Minho - Braga