Publicado no Encontro de Saberes 2015
Evento: XXIII Seminário de Iniciação Científica
Área:
Subárea:
| Título |
| PROJETO E IMPLEMENTAÇÃO DE UMA LINGUAGEM DE PROGRAMAÇÃO PARA DESENVOLVIMENTO DE SISTEMAS EMBARCADOS CORRETOS POR CONSTRUÇÃO |
| Autores |
|
RAUL FELIPE PIMENTA LOPES (Autor) RODRIGO GERALDO RIBEIRO (Orientador) |
| Resumo |
| Sistemas embarcados são ubíquos na sociedade moderna e estão presentes nos mais diversos dispositivos como celulares, aparelhos de GPS e em aplicações onde a corretude e segurança são fatores críticos como aplicações bancárias e dispositivos médicos. O desenvolvimento de softwares onde a corretude é um fator primordial é uma tarefa desafiadora pois, muitas vezes, deve-se lidar com detalhes do hardware. Por outro lado, para garantir um comportamento correto, incluindo propriedades de correção e segurança, o mesmo código de baixo nível deve ser representado por modelos abstratos que podem ser analisados rigorosamente por ferramentas como verificadores de modelos e assistentes de provas. Falhas em um sistema de software são um problema grave em qualquer domínio de aplicação, porém, as consequências de uma falha em softwares embarcados tendem a ser severas: mesmo simples erros na manipulação de detalhes de baixo nível de hardware podem comprometer o sistema por completo. Linguagens funcionais modernas como ML e Haskell provêem abstrações de alto nível e outros benefícios para aumentar a produtividade e reuso de código. Tais linguagens também fornecem garantias sobre tipos e gerenciamento de memória, automaticamente detectando e eliminando erros comuns em tempo de compilação, e, devido a sua fundamentação matemática, essas provêem oportunidades para a verificação e validação de software. Neste projeto, iniciamos o desenvolvimento de um compilador da linguagem ML para o Arduíno, formalizando a sintaxe, semântica e sistemas de tipos e desenvolvendo um protótipo do compilador para esta linguagem. O protótipo desenvolvido encontra-se em fase de testes para detectar possíveis inconsistências entre a implementação realizada e a formalização da linguagem. Como trabalhos futuros pretendemos estudar sistemas de tipos baseados em lógica linear para fornecer um controle preciso de alocação e liberação de memória, um problema crucial em desenvolvimento de sistemas embarcados. |
