FLASH-POSIX: DESENVOLVIMENTO FORMAL DE UM SISTEMA DE ARQUIVOS POSIX BASEADO EM MEMÓRIAS FLASH

Este projeto endereça este mini desafio e propõe o desenvolvimento formal de um sistema de arquivo verificável baseado em memórias flash, compatível com o padrão POSIX. O desafio aqui é gerar: (i) a especificação formal do comportamento das funcionalidades oferecidas pelo sistema de arquivos; (ii) a lista de suposições inerentes ao hardware escolhido; (iii) e o conjunto invariantes, assertions, e propriedades relativas às estruturas de dados e algoritmos utilizados na implementação do sistema de arquivos. Esta iniciativa visa potencializar a participação da UFBA no circuito de Métodos Formais. Com o desenvolvimento desse projeto, a UFBA passa a integrar uma comunidade de instituições de excelência que atuam em Métodos Formais.. Situação: Em andamento; Natureza: Pesquisa. Alunos envolvidos: Graduação: (6) . Integrantes: Adolfo Almeida Duran - Coordenador / Aline Maria Santos Andrade - Integrante. Financiador(es): Fundação de Amparo à Pesquisa do Estado da Bahia - Auxílio financeiro.

2008 - 2010