Made available in DSpace on 2015-03-03T15:47:45Z (GMT). No. of bitstreams: 1
ValerioGMJpdf.pdf: 1265506 bytes, checksum: f1fe3ef975bfeb2fce1dad3319a33f34 (MD5)
Previous issue date: 2009-09-09 / 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 / Este trabalho apresenta um m?todo de projeto proposta para veri ca??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
desa os 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 veri ca??o at? n?vel de assembly. A m 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 signifi cativa dessas atividades pode ser
automatizada atrav?s de um compilador espec?fi co. Para esse m, 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 veri ca??o
formal: acelerando o processo de verifica??o, reduzindo o tempo de projeto e aumentando
a qualidade e con fian?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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18679 |
| Date | 09 September 2009 |
| Creators | Medeiros J?nior, Val?rio Gutemberg de |
| Contributors | CPF:00809085437, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5, Moreira, Anamaria Martins, CPF:82573611787, http://lattes.cnpq.br/5861361541278876, Cavalcanti, Ana L?cia Caneca, CPF:54499925487, http://lattes.cnpq.br/9213785092326881, Maitelli, Andr? Laurindo, CPF:42046637100, http://lattes.cnpq.br/0477027244297797, D?harbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0025 seconds