| Designação | Código | Curso | Regime | Regente |
|---|
Programação Ciber-Física | 14612 [ME78ME7800006551] | Mestrado em Engenharia Informática [MEINF] | S2 | Renato Jorge Araújo Neves |
Objetivos | A UC progride do básico para o complexo através de exemplos do mundo real. A UC começa com um modelo básico e apresenta a respectiva semântica e noções de bisimulação (aproximada). Este material é então usado para investigar os principais aspectos do domínio ciber-físico: eg funções Càdlàg), comportamento Zeno e algoritmia de acessibilidade aproximada. Complementa-se com uma abordagem prática às ferramentas Uppaal e dReach.
Como o objectivo é abordar sistemas ciber-físicos de larga escala, estuda-se a programação ciber-física, que enfatiza composicionalidade. De forma a que o aluno possa analisar sistemas ciber-físicos rigorosamente, apresentam-se semânticas operacionais e denotacionais para a programação ciber-física, via estruturas categoriais e axiomáticas ensinadas na UC Cálculo e síntese de programas”, relacionando-se a computação ciber-física com a computação clássica e quântica. Complementa-se com uma abordagem prática à ferramenta Lince. |
Programa | 1. Autómatos híbridos como modelo base para a computação ciber-física; Noção de simulação e bissimulação.
2. Utilização deste modelo para abordar diversos aspectos da computação ciber-física.
3. As ferramentas Uppaal e dReach; Casos de estudo.
4. Programação ciber-física: Princípios algorítmicos e composicionalidade.
5. Semântica operacional e denotacional da programação ciber-física.
6. A ferramenta Lince; Casos de estudo. |
Bibliografia | The theory of hybrid automata. T. A. Henzinger. Published in the Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS), 1996.
Verification and control of hybrid systems. Paulo Tabuada. Published by Springer, 2009; ISBN: 978-1-4419-0223-8.
Logical foundations of cyber-physical systems. André Platzer. Published by Springer, 2018; ISBN: 978-3-319-63587-3.
The formal semantics of programming languages. Glynn Winskel. Published by MIT Press, 1993. ISBN: 978-0-262-23169-5.
An adequate while-language for hybrid computation. Sergey Goncharov and Renato Neves. Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages (PPDP), 2019. |
Resultados da aprendizagem | O objectivo da UC é preparar o aluno para a engenharia de sistemas ciber-físicos - princípios básicos, modelos de computação adequados e respectivas ferramentas. No final da aprendizagem o aluno deverá ser capaz de:
- Compreender e usar modelos standard de computação ciber-física, nomeadamente (extensões de) autómatos híbridos e linguagens de programação híbridas
- Entender as diferenças entre as várias noções de equivalência para estes dois modelos
- Reconhecer e tratar adequadamente o comportamento de Zeno
- Ser proficiente no uso das ferramentas Uppaal, dReach e Lince, que abrangem model-checking e teste/simulação
- Compreender as limitações do estado da arte e as possíveis consequências da sua resolução
- Coordenar adequadamente os resultados de aprendizagem anteriores para desenvolver e analisar de forma sistemática sistemas ciber-físicos complexos |
Método de avaliação | A avaliação tem uma componente teórica e uma prática. A primeira consiste em dois testes escritos, um sobre autómatos híbridos e outro sobre programação ciber-física. A última avalia a participação e projectos individuais relativos à engenharia de sistemas ciber-físicos para problemas do mundo real (e.g. aterrar uma nave espacial em segurança). |
Funcionamento | Turno: T 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 15. |
Departamento de Informática (UM)