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

Mostrar outras versões (1)

Resumo:Este trabalho apresenta um método de projeto proposta para verificaçã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 Petroleu...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Principais autores:	Medeiros Júnior, Valério Gutemberg de., Déharbe, David Boris Paul., Universidade Federal do Rio Grande do Norte.
Formato:	Dissertação
Publicado em:
Assuntos:	Engenharia de software - Dissertação. Métodos formais - Linguagem Assembly - Sistema embarcado - Software engineering. Formal methods. Assembly language. Embedded system.
Endereço do item:	https://app.bczm.ufrn.br/home/#/item/130090
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	oai:localhost:123456789-91965
record_format	dspace
spelling	oai:localhost:123456789-919652022-11-30T13:28:11Z Aplicação do método B ao projeto formal de software embarcado/ Medeiros Júnior, Valério Gutemberg de. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte. Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem Assembly - Dissertação. Sistema embarcado - Dissertação. Software engineering. Formal methods. Assembly language. Embedded system. Resumo:Este trabalho apresenta um método de projeto proposta para verificaçã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 desafios 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 verificaçã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 con ança do produto de software final. Todas essas qualidades são bastante relevantes para sistemas que envolvem sérios riscos ou exigem alta confiança, os quais são muito comuns na indústria do petróleo.#$&Abstract:This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler . Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry 1 2022-10-05T22:03:42Z 2022-10-05T22:03:42Z 2009. Dissertação 004.41 M488a DISSERT 130090 https://app.bczm.ufrn.br/home/#/item/130090 https://app.bczm.ufrn.br/home/#/item/130090
institution	Acervo SISBI
collection	SIGAA
topic	Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem Assembly - Dissertação. Sistema embarcado - Dissertação. Software engineering. Formal methods. Assembly language. Embedded system.
spellingShingle	Engenharia de software - Dissertação. Métodos formais - Dissertação. Linguagem Assembly - Dissertação. Sistema embarcado - Dissertação. Software engineering. Formal methods. Assembly language. Embedded system. Medeiros Júnior, Valério Gutemberg de. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte. Aplicação do método B ao projeto formal de software embarcado/
description	Resumo:Este trabalho apresenta um método de projeto proposta para verificaçã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 desafios 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 verificaçã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 con ança do produto de software final. Todas essas qualidades são bastante relevantes para sistemas que envolvem sérios riscos ou exigem alta confiança, os quais são muito comuns na indústria do petróleo.#$&Abstract:This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler . Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry
format	Dissertação
author	Medeiros Júnior, Valério Gutemberg de. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte.
author_facet	Medeiros Júnior, Valério Gutemberg de. Déharbe, David Boris Paul. Universidade Federal do Rio Grande do Norte.
author_sort	Medeiros Júnior, Valério Gutemberg de.
title	Aplicação do método B ao projeto formal de software embarcado/
title_short	Aplicação do método B ao projeto formal de software embarcado/
title_full	Aplicação do método B ao projeto formal de software embarcado/
title_fullStr	Aplicação do método B ao projeto formal de software embarcado/
title_full_unstemmed	Aplicação do método B ao projeto formal de software embarcado/
title_sort	aplicação do método b ao projeto formal de software embarcado/
publishDate	2022
url	https://app.bczm.ufrn.br/home/#/item/130090
work_keys_str_mv	AT medeirosjuniorvaleriogutembergde aplicacaodometodobaoprojetoformaldesoftwareembarcado AT deharbedavidborispaul aplicacaodometodobaoprojetoformaldesoftwareembarcado AT universidadefederaldoriograndedonorte aplicacaodometodobaoprojetoformaldesoftwareembarcado
_version_	1766828792047730688

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

Registros relacionados