Aplicação do método B ao projeto formal de software embarcado
AUTOR(ES)
Valério Gutemberg de Medeiros Júnior
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
Documentos Relacionados
- Metodologia de projeto de software embarcado voltada ao teste
- Modelagem e verificação formal do software embarcado de um simulador de satélite
- Projeto e implementaÃÃo do software de sistema embarcado para rastreamento e telemetria de veÃculo.
- Esqueletotipação : um método para desenvolvimento de software embarcado baseado em modelos.
- Esqueletotipação : um método para desenvolvimento de software embarcado baseado em modelos.