Generating a Google Go framework from an Uppaal model


Dealing with concurrency and parallelism is hard. Using scientific tools, models can be created giving insight into the nature of concurrent structures. Using these models one can sometimes even prove that various conditions hold within the model. To prevent human error when implementing a given model, one might consider a scheme where the source code for the concurrent behavior is generated from the model. We will demonstrate the possibility of such a scheme, specifically to generate a Google Go code framework from Uppaal models, which allows for the quick testing and correct implementation of the process described in by the model. Furthermore we will show the use of such a scheme using a example. Finally we will informally argue the validity of the algorithm.

Bachelor’s Thesis