Checking of models built using a graphically based formal modelling language

This paper describes the RDT language and a transformation from RDT into Promela code (the input language of the SPIN model-checker) which can be performed automatically and illustrates the use of the technique with an example.