Model transformation from RoboSim to network of timed automata for UPPAAL | Current Project

This project investigates how to transform from RoboSim models to timed automata.

We propose a model transformation method based on TA patterns and mapping rules, and develop a real-time automatic transformation tool from RoboSim model to NTA model for UPPAAL. This work was successfully applied to the real case Alpha algorithm. The next steps are: 1. Automatic generation of properties for robots. 2. Propose a new DSML for modeling specific environment.
Gustavo Carvalho
Gustavo Carvalho
Lecturer @ CIn-UFPE (BR)

My research interests include formal specification/verification, and tools development.