No Dropbox podemos nos cadastrar e armazenar, em pastas, todo tipo de arquivo como música, filmes, etc. O Dropbox guarda arquivos, com data e hora do upload, última modificação, e usuário criador. Cada arquivo tem várias versões associadas a ele, que podem ser recuperadas e tornar-se novamente a versão atual. A vários dispositivos do usuário podem ser dadas autorizações para visualizar e modificar os arquivos da conta dele do dropbox. Arquivos podem ser adicionados, modificados ou removidos. Uma limitação é que um arquivo só pode ser modificado por um único usuário em cada momento. Mesmo que dois usuários tenham permissão de modificação. Além disso, um arquivo não pode ser modificado por um usuário e lido por outro ao mesmo tempo.
O projeto consiste de duas partes. Uma especificação em Alloy (arquivo .als) e uma especificação em NuSMV (arquivo .smv) de acordo com os requisitos do tema sorteado para o grupo.
A especificação em Alloy deverá incluir a descrição estrutural do sistema e pelo menos três propriedades (fatos mais importantes). Deverá também ter pelo menos 2 asserts como casos de teste.
A especificação em NuSMV deverá incluir a descrição comportamental do sistema e pelo menos 3 propriedades descritas em LTL que o sistema deve garantir.
Cada um dos temas possui um cliente, que é o contato chave pra tirar dúvidas sobre o projeto. Vocês podem usar o slack para isso, mas tentem pelo menos um encontro presencial com o cliente.