Departamento de Informática (UM)

Página de Unidade Curricular

DesignaçãoCódigoCursoRegimeRegente

Programação Ciber-Física

14612 [ME78ME7800006551]

Mestrado em Engenharia Informática [MEINF]

S2

Luís Manuel Dias Coelho Soares Barbosa

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: Luís Manuel Dias Coelho Soares Barbosa; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 15.

[ Outras UCs do Departamento ]