Return to search

Verificando a corretude de geradores automáticos de código

Made available in DSpace on 2014-06-12T15:57:28Z (GMT). No. of bitstreams: 2
arquivo3199_1.pdf: 729356 bytes, checksum: 6c269a282f3e408a30566d12c64fac0e (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2011 / 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

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2373
Date31 January 2011
CreatorsSOUSA, Thiers Garretti Ramos
ContributorsMOTA, Alexandre Cabral
PublisherUniversidade Federal de Pernambuco
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Sourcereponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0022 seconds