Utilize este identificador para referenciar este registo: https://hdl.handle.net/10316/35590
Título: Geração Automática de Código Fonte a Partir de Modelos Formais
Autor: Martins, Miguel Antonio Rodrigues Lopes 
Orientador: Barbosa, Raul André Brajczewski
Palavras-chave: Java; JavaCC; Model checking; Network simulation; OMNeT++; PROMELA; PROMNeT++; Round-based consensus protocols; Source code generation; Spin
Data: 13-Set-2013
Título da revista, periódico, livro ou evento: Geração Automática de Código Fonte a Partir de Modelos Formais
Local de edição ou do evento: Coimbra
Resumo: The work presented/associated with this document relates to an area of computer science that is described as the generation of source code from the speci cation of a formal model, which shall be referred to as \Code Generation from Formal Models". This area is associated with two background areas, one of which being the area of \Model Checking". Model Checking, as described by Edmund M. Clarke et al.[1], is \a technique for verifying - nite state concurrent systems such as sequential circuit designs and communication protocols". This technique is appropriate for distributed and concurrent systems, since it aids developers in minimizing certain types of risks, such as the possibility that a deadlock will occur in the system at some point in time, preventing further progress, or the occurrence of a race condition. Given that only a model of a system is veri ed, but not the system itself, it naturally follows that it would be useful to generate source code from the model speci cation. This work thus encompasses the generation of source code from PROMELA models, veri ed by the Spin model checker. In its essence, this project attempts to answer the following question: is it possible to generate runnable source code from PROMELA models related to round-based consensus protocols? The short answer to it is \yes, with limitations".
Descrição: Dissertação de Mestrado em Engenharia Informática apresentada à Faculdade de Ciências e Tecnologia da Universidade de Coimbra
URI: https://hdl.handle.net/10316/35590
Direitos: openAccess
Aparece nas coleções:UC - Dissertações de Mestrado
FCTUC Eng.Informática - Teses de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato
Geraco Automatica de Codigo Fonte a Partir de Modelos Formais.pdf595.27 kBAdobe PDFVer/Abrir
Mostrar registo em formato completo

Visualizações de página 50

522
Visto em 26/mar/2024

Downloads

236
Visto em 26/mar/2024

Google ScholarTM

Verificar


Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.