Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-06-15T20:18:58Z
No. of bitstreams: 1
SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-06-18T19:19:46Z (GMT) No. of bitstreams: 1
SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5) / Made available in DSpace on 2018-06-18T19:19:46Z (GMT). No. of bitstreams: 1
SamuelLincolnMagalhaesBarrocas_TESE.pdf: 4123420 bytes, checksum: 746539c9cf569cfefe66e16e60516a7d (MD5)
Previous issue date: 2018-02-22 / O uso de Geradores Automáticos de Código para Métodos Formais não apenas minimiza
esforços na implementação de Sistemas de Software, como também reduz a chance
da existência de erros na execução destes Sistemas. Estas ferramentas, no entanto, podem
ter faltas em seus códigos-fonte que causam erros na geração dos Sistemas de Software,
e então a verificação de tais ferramentas é encorajada. Esta tese de Doutorado visa criar
e desenvolver uma estratégia para verificar JCircus, um Gerador Automático de Código
de um amplo sub-conjunto de Circus para Java. O interesse em Circus vem do fato de
que ele permite a especificação dos aspectos concorrentes e de estado de um Sistema de
maneira direta. A estratégia de verificação consiste nos seguintes passos: (1) extensão da
Semântica Operacional de Woodcock e prova de que ela é sólida com respeito à Semântica
Denotacional existente de Circus na Teoria Unificada de Programação (UTP), que é um
framework que permite prova e unificação entre diferentes teorias; (2) desenvolvimento e
implementação de uma estratégia que verifica o refinamento do código gerado por JCircus,
através de uma toolchain que engloba um Gerador de Sistema de Transições Rotuladas
com Predicado (LPTS) para Circus e um Gerador de Modelos que aceita como entrada
(I) o LPTS e (II) o código gerado por JCircus, e gera um modelo em Java Pathfinder que
verifica o refinamento do código gerado por JCircus. Através da aplicação do passo (2)
combinada com técnicas baseadas em cobertura no código fonte de JCircus, nós visamos
aumentar a confiabilidade do código gerado de Circus para Java. / The use of Automatic Code Generators for Formal Methods not only minimizes efforts
on the implementation of Software Systems, but also reduces the chance of existing errors
on the execution of such Systems. These tools, however, can themselves have faults on
their source codes that may cause errors on the generation of Software Systems, and thus
verification of such tools is encouraged. This PhD thesis aims at creating and developing a
strategy to verify the code generation from the Circus formal method to Java Code. The
interest in Circus comes from the fact that it allows the specification of concurrent and
state-rich aspects of a System in a straightforward manner. The code generation envisaged
to be verified is performed by JCircus, a tool that translates a large subset of Circus to Java
code that implements the JCSP API. The strategy of verification consists on the following
steps: (1) extension of Woodcock’s Operational Semantics to Circus processes and proof
that it is sound with respect to the Denotational Semantics of Circus in the Unifying
Theories of Programming (UTP), that is a framework that allows proof and unification of
different theories; (2) development and implementation of a strategy that refinement-checks
the code generated by JCircus, through a toolchain that encompasses (2.1) a Labelled
Predicate Transition System (LPTS) Generator for Circus and (2.2) a Model Generator that
inputs (I) a LPTS and (II) the code generated by JCircus, and generates a model (that
uses the Java Pathfinder code model-checker) that refinement-checks the code generated
by JCircus. Combined with coverage-based techniques on the source code of JCircus,
we envisage improving the reliability of the Code Generation from Circus to Java.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/25443 |
| Date | 22 February 2018 |
| Creators | Barrocas, Samuel Lincoln Magalhães |
| Contributors | 02386943488, Musicante, Martin Alejandro, 82500304434, Costa, Umberto Souza Da, 72031220500, Mota, Alexandre Cabral, 73547735491, Gomes, Bruno Emerson Gurgel, 01061676420, Oliveira, Marcel Vinicius Medeiros |
| Publisher | PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| 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.0019 seconds