Geração Automática de Código Fonte a Partir de Modelos Formais

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".