| Designação | Código | Curso | Regime | Regente |
|---|
Computação Ciber-Física | 14925 [ME80ME8002006775] | Mestrado em Engenharia Física [MEF] | 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 | Tabuada, P. (2009). Verification and control of hybrid systems, Springer.
Platzer, A. (2018). Logical foundations of cyber-physical systems, Springer.
Winskel, G. (1993). The formal semantics of programming languages. MIT Press. |
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:
1. 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
2. Entender as diferenças entre as várias noções de equivalência para estes dois modelos
3. Reconhecer e tratar adequadamente o comportamento de Zeno
4. Ser proficiente no uso das ferramentas Uppaal, dReach e Lince, que abrangem model-checking e teste/simulação
5. Compreender as limitações do estado da arte e as possíveis consequências da sua resolução
6. Coordenar adequadamente os resultados de aprendizagem anteriores para desenvolver e analisar de formasistemática sistemas ciber-físicos complexos |
Método de avaliação | A avaliação tem uma componente teórica (vale entre 60-70%) e uma prática (vale 30-40%). 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: Norihiro Yamada; Dep.: DI; Horas: 15.
Turno: TP 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 15. |
Departamento de Informática (UM)