Adding uncertainty to real-time programming

Abstract

In this dissertation we cover the implementation in Haskell of an interpreter for a while-language capable of handling both hybrid and probabilistic effects. The interpreter is supported by both operational and denotational semantics which were devised in this dissertation as well. We started by studying a pre-existing syntax and operational semantics of a programming language capable of performing wait calls and probabilistic choices through a random-number-generator. We then redefined this semantics to another one that is more suitable for statistical analysis in programming. Next we performed another iteration over these two semantics, more specifically we extended them to support full hybrid behaviour, traditionally used to encode interactions between digital devices and physical processes such as movement and time. We also devised two denotational semantics corresponding to the operational semantics mentioned before, as a way of providing a mathematical abstraction, through the use of monads, to the programs of our language. Not only this, we also implemented a domain specific language embedded into Haskell, which thus provides to the hybrid programmer all the expressive power that Haskell offers in addition to a palette of combinators designed specifically for the hybrid domain. Such gives rise to an expressivity power much greater than what the aforementioned while-language can provide. Lastly, we presented and analysed several deterministic hybrid programs, such as cruise controllers, and added subtle probabilistic elements to them that reflect certain real-word scenarios. Such an addition lead from one possible execution to several possible executions; and most notably some of the latter revealed safety issues introduced by the probabilistic elements. All in all this dissertation has both theoretical and practical contributions that form a stepping stone towards a rigorous engineering discipline of probabilistic hybrid systems.

Através desta dissertação descrevemos uma implementação em Haskell de um interpretador para uma linguage while capaz de lidar tanto com o efeito híbrido como com o efeito probabilístico. O interpretador é suportado por semânticas operacionais e denotacionais que foram definidas também nesta dissertação. Primeiramente, abordamos uma sintaxe e semântica operacional pré-existentes de uma linguagem capaz de realizar chamadas de espera e escolhas probabilísticas, através de um gerador de números aleatórios. De seguida, redefinimos esta semântica numa outra que é mais apropriada para a análise estatística dos programas. Consequentemente, realizamos uma outra iteração sobre estas semânticas sendo que as estendemos para suportarem totalmente o comportamento híbrido, tradicionalmente utilizado para representar interações entre dispositivos digitais e físicos, tais como movimento e tempo. Criámos também duas semânticas denotacionais, correspondentes às semânticas anteriores, de modo a fornecer uma abstração matemática, através da utilização de mónadas, para os possíveis programas da nossa linguagem. Para além disto, foi implementada uma domain specific language incorporada em Haskell, o que providencia ao programador híbrido todo o poder que o Haskell oferece conjugado com combinadores definidos especialmente para o domínio híbrido. Tal dá origem a um poder expressivo muito maior do que aquele que a linguagem while supramencionada pode providenciar. Por fim, abordaram-se vários exemplos de programas híbridos determinísticos, tais como sistemas de cruise control, aos quais foram adicionados elementos probabilísticos subtis que refletem cenários do mundo real. Esta adição fez com que fossemos de uma execução para uma variedade de execuções possíveis; e mais notávelmente alguns dos sistemas revelaram problemas relacionados com a segurança quando os elementos probabílisticos foram introduzidos. Em suma, esta dissertação apresenta contribuições teóricas e práticas que se traduzem num passo em direção a uma dísciplina de engenharia rigorosa sobre sístemas híbridos probabilísticos.