| dc.contributor | MOTA, Alexandre Cabral | |
| dc.creator | SOUSA, Thiers Garretti Ramos | |
| dc.date | 2014-06-12T15:57:28Z | |
| dc.date | 2014-06-12T15:57:28Z | |
| dc.date | 2011-01-31 | |
| dc.identifier | Garretti Ramos Sousa, Thiers; Cabral Mota, Alexandre. Verificando a corretude de geradores automáticos de código. 2011. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2011. | |
| dc.identifier | https://repositorio.ufpe.br/handle/123456789/2373 | |
| dc.description | Os contratos (modelos que descrevem mais detalhadamente a arquitetura e os componentes)
podem ser utilizados para a construção de softwares corretos. Esta construção pode ser realizada
através do (1) cálculo de refinamento, (2) refinamento da estratégia e (3) fazendo a
geração automática de código. Embora (1) e (2) são soluções corretamente comprovadas, eles
requerem bastante esforço. Por outro lado, (3) é uma solução mais simples para derivação do
código. No entanto, esta solução não pode fornecer um código confiável em relação aos seus
contratos (ao menos que se comprove que o gerador de código é correto). Este trabalho propõe
uma estratégia de testes baseados em modelos para verificar se determinado gerador de código
é correto. A estratégia inicia-se com JML (linguagem baseada em contrato utilizada no Java)
usando como estudo de caso o JavaCard, JMLe (um gerador de código baseado em JML) e o
Jartege (gerador de testes baseados em modelos). Além disso, através deste trabalho é realizado
um experimento onde é investigado o número de erros encontrados no jmle variando os valores
do parâmetros do Jartege no nosso estudo de caso | |
| dc.format | application/pdf | |
| dc.language | por | |
| dc.publisher | Universidade Federal de Pernambuco | |
| dc.subject | jmle | |
| dc.subject | Testes baseados em modelos | |
| dc.subject | Especificações Formais | |
| dc.title | Verificando a corretude de geradores automáticos de código | |
| dc.type | masterThesis | |
