Please use this identifier to cite or link to this item: https://hdl.handle.net/10316/35590
Title: Geração Automática de Código Fonte a Partir de Modelos Formais
Authors: Martins, Miguel Antonio Rodrigues Lopes 
Orientador: Barbosa, Raul André Brajczewski
Keywords: Java; JavaCC; Model checking; Network simulation; OMNeT++; PROMELA; PROMNeT++; Round-based consensus protocols; Source code generation; Spin
Issue Date: 13-Sep-2013
Serial title, monograph or event: Geração Automática de Código Fonte a Partir de Modelos Formais
Place of publication or event: Coimbra
Abstract: 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".
Description: 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
Rights: openAccess
Appears in Collections:UC - Dissertações de Mestrado
FCTUC Eng.Informática - Teses de Mestrado

Files in This Item:
Show full item record

Page view(s) 50

522
checked on Mar 26, 2024

Download(s)

236
checked on Mar 26, 2024

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.