Departamento de Informática (UM)

Página de Unidade Curricular

DesignaçãoCódigoCursoRegimeRegente

Computação Ciber-Física

14925 [ME80ME8002006775]

Mestrado em Engenharia Física - Área de Especialização em Física da Informação [MEF]

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

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: Renato Jorge Araújo Neves; Dep.: DI; Horas: 30.

[ Outras UCs do Departamento ]