Aplicação do método B ao projeto formal de software embarcado

AUTOR(ES)
DATA DE PUBLICAÇÃO

2009

RESUMO

Este trabalho apresenta um método de projeto proposta para vericação formal do modelo funcional do software até o nível da linguagem assembly. Esse método é fundamentada no método B, o qual foi desenvolvido com o apoio e interesse da multinacional do setor de petróleo e gás British Petroleum (BP). A evolução dessa metodologia tem como objetivo contribuir na resposta de um importante problema, que pertence aos grandes desaos da computação, conhecido como The Verifying Compiler . Nesse contexto, o presente trabalho descreve um modelo formal do microcontrolador Z80 e um sistema real da área de petróleo. O modelo formal do Z80 foi desenvolvido e documentado, por ser um pré-requisito para a vericação até nível de assembly. Afim de validar e desenvolver a metodologia citada, ela foi aplicada em um sistema de teste de produção de poços de petróleo, o qual é apresentado neste trabalho. Atualmente, algumas atividades são realizadas manualmente. No entanto, uma parte significativa dessas atividades pode ser automatizada através de um compilador específico. Para esse fim, a modelagem formal do microcontrolador e a modelagem do sistema de teste de produção fornecem conhecimentos e experiências importantes para o projeto de um novo compilador. Em suma, esse trabalho deve melhorar a viabilidade de um dos mais rigorosos critérios de verificação formal: acelerando o processo de verificação, reduzindo o tempo de projeto e aumentando a qualidade e conança do produto de software final. Todas essas qualidades são bastante relevantes para sistemas que envolvem sérios riscos ou exigem alta conança, os quais são muito comuns na indústria do petróleo

ASSUNTO(S)

sistemas de computacao verified compilation, b method formal methods software engineering engenharia de software verificação de assembly método b métodos formais

ACESSO AO ARTIGO

Documentos Relacionados