Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/56808
Título: | Hybrid programs |
Autor(es): | Neves, Renato Jorge Araújo |
Orientador(es): | Barbosa, L. S. Martins, Manuel António |
Data: | 22-Jun-2018 |
Resumo(s): | 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. Esta tese estuda sistemas híbridos, uma família emergente de dispositivos que envolvem diferentes interações entre computações digitais e processos físicos. Estes sistemas estão rapidamente a tornar-se elementos-chave da engenharia de software, o que é explicado pela necessidade de desenvolver produtos que interagem com os atributos físicos do seu ambiente e. g. velocidade, tempo, energia, e temperatura – exemplos típicos variam de micro-sensores e pacemakers, a veículos autónomos, infra-estruturas de transporte, e redes eléctricas distritais. Mas ainda que amplamente usados, estes sistemas são geralmente desenvolvidos de forma pouco sistemática nas prácticas de programação atuais. O objetivo deste trabalho é isolar as interações básicas entre computações digitais e processos físicos, e subsequentemente desenvolver o paradigma de programação subjacente. Para fazer isto de forma precisa, a nossa base de trabalho irá ser a teoria das mónadas, uma estrutura categórica para o desenvolvimento sistemático de semânticas na programação. A partir desta base, provamos a existência de uma mónada que capta as interações acima mencionadas, e usamo-la para desenvolver e examinar os fundamentos do paradigma de programação correspondente a que chamamos programação híbrida: mostramos como construir, de maneira metódica, diferentes linguagens de programação que acomodam amplificadores, equações diferenciais, e atribuições - os ingredientes básicos dos sistemas híbridos - caracterizamos todas as operações sobre programas disponíveis, introduzimos construções if-then-else, operações para lidar com excepções, e diferentes tipos de feedback. Os sistemas híbridos trazem vários aspectos da teoria de controlo para a ciência da computação. Um destes é a noção de estabilidade, que se refere à capacidade de um sistema de evitar mudanças drásticas no seu output se pequenas variações no seu estado ou input ocorrerem. Neste trabalho, desenvolvemos uma noção composicional de estabilidade para a programação híbrida. Introduzimos também programas híbridos com memória interna, que formam a base de uma disciplina de desenvolvimento de software baseado em componentes. Desenvolvemos a sua teoria coalgébrica, nomeadamente linguagens, noções de comportamento e bisimulação. Neste processo, introduzimos também novos resultados teóricos sobre Coalgebra, incluindo melhorias a resultados conhecidos e provas acerca da existência de noções de comportamento para sistemas de transição não determinísiticos com espaço de estados infinitos. |
Tipo: | Tese de doutoramento |
Descrição: | The MAP-i Doctoral Programme in Informatics, of the Universities of Minho, Aveiro and Porto |
URI: | https://hdl.handle.net/1822/56808 |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Renato Jorge Araujo Neves.pdf | 5,31 MB | Adobe PDF | Ver/Abrir |