Translating Uppaal to Not Quite C
Martijn Hendriks · Radboud Repository (Radboud University) · 2001
A bstract.This project presents a simple translation from Uppaal models of real-time controllers to NQC programs.The modeling of these controllers in Uppaal provides a way to verify the requirements on these controllers.The user directs the translation by defining a type for each variable used in the model and by assigning each automaton in the model to a controller.The translation, that has been implemented in the tool uppaal2nqc, results in a set of NQC programs that, when all NQC programs are run concurrently, approximately realizes a subset of the executions of the model.An Uppaal model of controllers of an experimental LEGO setup has been translated and the resulting NQC programs have been run in this setup to validate the translation.