Navegando por Autor "Barrocas, Samuel Lincoln Magalhães"
Agora exibindo 1 - 2 de 2
- Resultados por página
- Opções de Ordenação
Dissertação JCircus 2.0: Uma extensão da ferramenta de tradução de Circus para Java(Universidade Federal do Rio Grande do Norte, 2011-08-29) Barrocas, Samuel Lincoln Magalhães; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255; ; http://lattes.cnpq.br/3124946268301438; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244Esta dissertação tem como objetivo estender a ferramenta JCircus, um tradutor de especificações formais para código que recebe uma especificação em Circus como entrada, e traduz a especificação para código Java. Circus é uma linguagem formal cuja sintaxe é baseada nas sintaxes das linguagens Z e CSP. O código gerado por JCircus faz uso de JCSP, que é uma API de Java que implementa primitivas de CSP. O fato de JCSP não implementar CSP completamente faz com que a estratégia de tradução de Circus para Java seja não-trivial. Algumas primitivas de CSP, como paralelismo, escolhas externa e interna, comunicação, e multi-sincronização são implementadas em JCSP de forma parcial. Nesta dissertação, estendemos a tradução destas primitivas. Além disso, esta dissertação também desenvolverá uma ferramenta para fazer testes em processos JCSP, chamada JCSPUnit.Tese A strategy to verify the code generation from concurrent and state-rich circus specifications to executable code(2018-02-22) Barrocas, Samuel Lincoln Magalhães; Oliveira, Marcel Vinicius Medeiros; ; ; Musicante, Martin Alejandro; ; Costa, Umberto Souza Da; ; Mota, Alexandre Cabral; ; Gomes, Bruno Emerson Gurgel;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.