utwente-fmt / UrPal

UPPAAL Sanity Checker
5 stars 1 forks source link

MPS front-end for Uppaal #21

Open ramononis opened 5 years ago

ramononis commented 5 years ago

Possible (BIG) master project?

Problem UrPal attempts to give sanity checks as seen in modern IDEs to Uppaal.
While model transformations, property verification and simple static analysis is enough for some sanity checks, more advanced sanity checks based on data/control flow analysis, are beyond what can be easily made in the current Uppaal front-end using the current frameworks (EMF).
Also, modern IDEs have many more features that can be applied to an Uppaal front-end:

To implement this into UrPal would require one to work around the many limitations that the current architecture has.
Solution The approach we propose in this issue is to develop an alternative Uppaal front-end using JetBrains MPS.
MPS (meta programming system) is an open-source software tool used to make (domain specific) languages. Differently from traditional text-based languages, MPS-generated languages are edited directly on the AST, instead of on the plain-text representation. This allows us to begin with the existing Uppaal model, and define the editor for this model in any way we want.
In short the following steps need to be made: