CSI/2025-26

CSI/2025-26/Método B

Trabalho de Grupo

Introdução

O tema deste trabalho prático (TP) de grupo é o que abaixo se descreve, estando ainda aberta a possibilidade, por parte dos grupos, de proporem temas mais específicos, sintonizados com os seus interesses (“but time is running out…”).

Os grupos devem:

• Fazer um estudo da referência bibliográfica apresentada.
• Preparar slides para uma apresentação oral do trabalho (20 min + 10 de discussão) a ter lugar na semana de 26 a 30 de Janeiro.
• Preparar cuidadosamente essa defesa oral, equilibrando bem a participação dos três elementos do grupo.

Notas:

• Não há lugar à escrita de um relatório.
• Valorizar-se-ão os trabalhos em que tenha sido aplicado o método de especificação relacional estudado nesta UC.
• Sugere-se o recurso ao Alloy Analyser para validar a formalização a fazer, sem prejuízo de se poderem usar outras ferramentas que se considerem adequadas.

Tema

O tema deste TP é o de especificar um controlador de segurança para condução autónoma em auto-estradas.

De acordo com os requisitos da referência bibliográfica abaixo, a ideia é considerar-se apenas uma faixa na auto-estrada, onde cada veículo pode acelerar e travar. O objetivo é manter a distância de segurança para o veículo da frente. Se o tempo der, poderá ser abordada a situação de uma auto-estrada com múltiplas faixas, onde cada veículo também pode mudar de faixa.

Deverão ser especificadas as relações em jogo, os invariantes do problema e os argumentos de segurança. Os detalhes técnicos deverão ser encapsulados em funções auxiliares.

Nota: este tema foi proposto como case-study na conferência ABZ’25, podendo ser encontrada neste site informação adicional.

Referência: Michael Leuschel, Fabian Vu and Kristin Rutenkolk. Case Study: Safety Controller for Autonomous Driving on Highways. Versão 3 neste github.