Métodos Formais em Engenharia de Software |
---|
Cálculo de Sistemas de Informação |
Programação Ciber-física |
Verificação Formal |
Calendário | Sumários |
Anos anteriores |
Alumni |
Docente | Foto | Horário | Sala |
---|---|---|---|
Manuel Alcino Cunha | 5a-feira, 9h-11h | CP1 1.21 |
# | Nome | Curso | Grupo |
---|---|---|---|
a83916 | Ana João Dias de Almeida | MiEI | 5 |
a85516 | António Manuel Carvalho Gonçalves | MiEI | 9 |
a80453 | Bárbara Andreia Cardoso Ferreira | MiEI | |
a82529 | Carlos Manuel Marques Afonso | MiEI | 3 |
a34900 | Cecília da Conceição de Oliveira Soares | MiEI | 13 |
a67683 | César Eduardo da Silva Magalhães | MiEI | 7 |
pg41842 | César Hugo Moreira da Silva | MEI | 12 |
a80970 | Davide da Silva Matos | MiEI | 15 |
a76089 | Etienne da Silva Filipe Amado da Costa | MiEI | 11 |
a85731 | Gonçalo José Azevedo Esteves | MiEI | 9 |
a86617 | Gonçalo Pinto Nogueira | MiEI | 3 |
a81283 | Hugo Filipe Oliveira de Sousa Faria | MiEI | 1 |
a85573 | Jorge Gabriel Alves Cerqueira | MiEI | 5 |
a84776 | José Emanuel Silva Rodrigues | MiEI | 2 |
pg42839 | José Gonçalo Macedo Costa | MEI | 7 |
a84577 | José Pedro Oliveira Silva | MiEI | 14 |
a85954 | Luís Mário Macedo Ribeiro | MIEI | 14 |
a71407 | Maurício Zulueta Lima Salgado | MiEI | 10 |
a85700 | Pedro Miguel Araújo Costa | MiEI | 10 |
a84783 | Pedro Miguel Borges Rodrigues | MiEI | 14 |
a86266 | Rafael Inácio Lourenço | MiEI | 2 |
a75411 | Ricardo Guerra Leal | MiEI | 15 |
a81716 | Rodolfo António Vieira da Silva | MiEI | 1 |
a80789 | Rui Filipe Brito Azevedo | MiEI | 11 |
pg36086 | Vítor Hugo Gonçalves Silva | MMC | 6 |
O trabalho consiste em traduzir uma especificação feita em TLA+ para Electrum. Pode ser feito em grupos de até 3 elementos, mas espera-se que a extensão do trabalho realizado seja proporcional à dimensão do grupo. A entrega deverá ser feita por email até ao dia do teste (14 de Janeiro). O email deve explicar as principais opções tomadas e dificuldades sentidas, e incluir como anexo a especificação em Electrum, assim como o theme desenvolvido. Opcionalmente podem também fazer algumas comparações de performance entre as duas ferramentas.
Cada grupo deve optar por uma das seguintes especificações em TLA+. Agradeço que me informem logo que possível qual a constituição do grupo e especificação escolhida. No máximo cada especificação deverá ser trabalhada por 3 grupos, sendo a alocação de grupos a especificações publicada nesta página.
SimpleAllocator.tla
), uma com escalonamento (SchedullingAllocator.tla
), e uma especificação de uma implementação distribuída (AllocatorImplementation.tla
). Em função da dimensão do grupo e objectivo de nota podem optar por traduzir apenas uma ou mais destas especificações.Grupo | #1 | #2 | #3 | Entrega |
---|---|---|---|---|
1 | a81716 | a81283 | 12 Jan | |
2 | a86266 | a84776 | 13 Jan | |
3 | a86617 | a82529 | 14 Jan |
Grupo | #1 | #2 | #3 | Entrega |
---|---|---|---|---|
5 | a83916 | a85573 | 14 Jan | |
6 | pg36086 | 14 Jan | ||
7 | a67683 | pg42839 | 14 Jan |
Grupo | #1 | #2 | #3 | Entrega |
---|---|---|---|---|
9 | a85516 | a85731 | 14 Jan | |
10 | a85700 | a71407 | 14 Jan | |
11 | a76089 | a80789 | 13 Jan | |
12 | pg41842 | 13 Jan |
Voting.tla
) que especifica a ideia de usar votações para obter o consenso, e uma especificação de alto nível do algoritmo (Paxos.tla
). Em função da dimensão do grupo e objectivo de nota podem optar por traduzir apenas a primeira ou ambas as especificações.Grupo | #1 | #2 | #3 | Entrega |
---|---|---|---|---|
13 | a34900 | 14 Jan | ||
14 | a85954 | a84577 | a84783 | 13 Jan |
15 | a75411 | a80970 | 18 Jan |