RDT: A Graphical Formal Modelling Language
RDT is a formal modelling language able to describe distributed systems conceived and constructed by Bob Walters. What sets RDT apart is the way it uses diagrams in place of the usual process algebra. The motivation is that, whilst modellers interested in the process of modelling are happy to contend with them, many potential “real life” users of formal modelling techniques and non‑technical stakeholders in process descriptions find process algebras impossibly hard to use. In contrast, they generally find diagrams more palatable (even if they wouldn’t want to draw them). The objective of RDT was to create a modelling language/paradigm which would be attractive to non‑technical uses by using diagrams to describe models whilst retaining sufficient precision and formality to permit its models to be executed and for desired properties to be established using model checking software.
In contrast with many diagrammatic languages/systems, users of RDT are not expected to draw their own diagrams. Instead they use a tool to create their models. The primary purpose of the tool is to provide (novice) users with an interface to the language which permits them to create models quickly and easily (without major initial investment in learning the syntax of the language). The tool redraws the diagrams after each change or addition by the user. Also, rather than expecting names or values to be typed, it offers a choice of available values whenever possible. An additional benefit is that the tool constrains the user to creating models which are syntactically correct.
The style of the diagrams is illustrated above. Each model includes a collection of processes. Instances of these processes are then joined together in another diagram to form the complete system being modelled. The tool maintains an internal representation of the modellers work from which it generates and displays the diagrams as required. In addition to the model generation tool, there are also tools which are able to execute models and generate a representation of a model in Promela for checking using the SPIN model checker.
The language is described fully my thesis and the following
papers which are all available from my personal web pages or the
P. Henderson, R.J. Walters, and S. Crouch, “Implementing Hierarchical Features in a Graphically Based Formal Modelling Language,” 28th Annual International Computer Software and Applications Conference (COMPSAC 2004), Hong Kong, 2004, pp. 92-98.
R.J. Walters, “Automating Checking of Models built using a Graphically Based Formal Modelling Language,” Journal of Systems and Software, vol. 76, pp. 55-64, 2005.
R.J. Walters, “A Graphically Based Language for Constructing,
Executing and Analysing Models of Software Systems,” 26th Annual
International Computer Software and Applications Conference (COMPSAC 2002),
R.J. Walters, “A Graphically based language for
constructing, executing and analysing models of software systems,” in Electronics
and Computer Science. Southampton:
I don’t have a tested, packaged up version of RDT available for download at present. If you would like to try it, contact me at rjw1@ecs.soton.ac.uk and I will do my best to build one for you.
Page updated: 03 August 2005